Question

Say we add a new rule R*to the rules of SD, to form the larger system of rules SD*. For ease of expression, write Γ ⊢sd S for "S is derivable from Γ using the rules of SD " and Γ ⊢sd* S for "S is derivable from using the rules of SD*"

Answer 1

Admissibility has been systematically studied only in the case of structural rules in propositional non-classical logics, which we will describe next.

Let a set of basic propositional connectives be fixed (for instance, {\displaystyle \{\to ,\land ,\lor ,\bot \}}$\{\to ,\land ,\lor ,\bot \}$ in the case of superintuitionistic logics, or {\displaystyle \{\to ,\bot ,\Box \}}$\{\to ,\bot ,\Box \}$ in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p₀, p₁, …. A substitution σ is a function from formulas to formulas which commutes with the connectives, i.e.,

{\displaystyle \sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})}$\sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})$

for every connective f, and formulas A₁, …, A_n. (We may also apply substitutions to sets Γ of formulas, making σΓ = {σA: A ∈ Γ}.) A Tarski-style consequence relation^[1] is a relation {\displaystyle \vdash }$\vdash$between sets of formulas, and formulas, such that

1. {\displaystyle A\vdash A,}$A\vdash A,$
2. if {\displaystyle \Gamma \vdash A}$\Gamma \vdash A$ then {\displaystyle \Gamma ,\Delta \vdash A,}$\Gamma ,\Delta \vdash A,$
3. if {\displaystyle \Gamma \vdash A}$\Gamma \vdash A$ and {\displaystyle \Delta ,A\vdash B}$\Delta ,A\vdash B$ then {\displaystyle \Gamma ,\Delta \vdash B,}$\Gamma ,\Delta \vdash B,$

for all formulas A, B, and sets of formulas Γ, Δ. A consequence relation such that

4. if {\displaystyle \Gamma \vdash A}$\Gamma \vdash A$ then {\displaystyle \sigma \Gamma \vdash \sigma A}$\sigma \Gamma \vdash \sigma A$

for all substitutions σ is called structural. (Note that the term "structural" as used here and below is unrelated to the notion of structural rules in sequent calculi.) A structural consequence relation is called a propositional logic. A formula A is a theorem of a logic {\displaystyle \vdash }$\vdash$ if {\displaystyle \varnothing \vdash A}$\varnothing \vdash A$.

For example, we identify a superintuitionistic logic L with its standard consequence relation {\displaystyle \vdash _{L}}$\vdash _{L}$ axiomatizable by modus ponens and axioms, and we identify a normal modal logicwith its global consequence relation {\displaystyle \vdash _{L}}$\vdash _{L}$ axiomatized by modus ponens, necessitation, and axioms.

A structural inference rule^[2] (or just rule for short) is given by a pair (Γ,B), usually written as

{\displaystyle {\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,}${\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,$

where Γ = {A₁, …, A_n} is a finite set of formulas, and B is a formula. An instance of the rule is

{\displaystyle \sigma A_{1},\dots ,\sigma A_{n}/\sigma B}$\sigma A_{1},\dots ,\sigma A_{n}/\sigma B$

for a substitution σ. The rule Γ/B is derivable in {\displaystyle \vdash }$\vdash$, if {\displaystyle \Gamma \vdash B}$\Gamma \vdash B$. It is admissible if for every instance of the rule, σB is a theorem whenever all formulas from σΓ are theorems.^[3] In other words, a rule is admissible if, when added to the logic, does not lead to new theorems.^[4] We also write {\displaystyle \Gamma \,|\!\!\!\sim B}$\Gamma \,|\!\!\!\sim B$ if Γ/B is admissible. (Note that {\displaystyle |\!\!\!\sim }$|\!\!\!\sim$ is a structural consequence relation on its own.)

Every derivable rule is admissible, but not vice versa in general. A logic is structurally complete if every admissible rule is derivable, i.e., {\displaystyle {\vdash }={\,|\!\!\!\sim }}${\vdash }={\,|\!\!\!\sim }$.^[5]

In logics with a well-behaved conjunction connective (such as superintuitionistic or modal logics), a rule {\displaystyle A_{1},\dots ,A_{n}/B}$A_{1},\dots ,A_{n}/B$ is equivalent to {\displaystyle A_{1}\land \dots \land A_{n}/B}$A_{1}\land \dots \land A_{n}/B$ with respect to admissibility and derivability. It is therefore customary to only deal with unary rules A/B.

Examples[edit]

• Classical propositional calculus (CPC) is structurally complete.^[6] Indeed, assume that A/B is non-derivable rule, and fix an assignment v such that v(A) = 1, and v(B) = 0. Define a substitution σ such that for every variable p, σp = {\displaystyle \top }$\top$ if v(p) = 1, and σp = {\displaystyle \bot }$\bot$ if v(p) = 0. Then σA is a theorem, but σB is not (in fact, ¬σB is a theorem). Thus the rule A/B is not admissible either. (The same argument applies to any multi-valued logic L complete with respect to a logical matrix whose all elements have a name in the language of L.)
• The Kreisel–Putnam rule (a.k.a. Harrop's rule, or independence of premise rule)

{\displaystyle ({\mathit {KPR}})\qquad {\frac {\neg p\to q\lor r}{(\neg p\to q)\lor (\neg p\to r)}}}$({\mathit {KPR}})\qquad {\frac {\neg p\to q\lor r}{(\neg p\to q)\lor (\neg p\to r)}}$

is admissible in the intuitionistic propositional calculus (IPC). In fact, it is admissible in every superintuitionistic logic.^[7] On the other hand, the formula

{\displaystyle (\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))}${\displaystyle (\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))}$

is not an intuitionistic tautology, hence KPR is not derivable in IPC. In particular, IPC is not structurally complete.

• The rule

{\displaystyle {\frac {\Box p}{p}}}${\frac {\Box p}{p}}$

is admissible in many modal logics, such as K, D, K4, S4, GL (see this table for names of modal logics). It is derivable in S4, but it is not derivable in K, D, K4, or GL.

• The rule

{\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}}${\frac {\Diamond p\land \Diamond \neg p}{\bot }}$

is admissible in every normal modal logic.^[8] It is derivable in GL and S4.1, but it is not derivable in K, D, K4, S4, S5.

• Löb's rule

{\displaystyle ({\mathit {LR}})\qquad {\frac {\Box p\to p}{p}}}$({\mathit {LR}})\qquad {\frac {\Box p\to p}{p}}$

is admissible (but not derivable) in the basic modal logic K, and it is derivable in GL. However, LR is not admissible in K4. In particular, it is not true in general that a rule admissible in a logic L must be admissible in its extensions.

• The Gödel–Dummett logic (LC), and the modal logic Grz.3 are structurally complete.^[9] The product fuzzy logic is also structurally complete.