Editing Admissible rule (section)

==Definitions==

Admissibility has been systematically studied only in the case of structural (i.e. [[substitution (logic)|substitution]]-closed) rules in [[propositional logic|propositional]] [[non-classical logic]]s, which we will describe next.

Let a set of basic [[logical connective|propositional connective]]s be fixed (for instance, <math>\{\to,\land,\lor,\bot\}</math> in the case of [[superintuitionistic logic]]s, or <math>\{\to,\bot,\Box\}</math> in the case of [[modal logic|monomodal logic]]s). [[Well-formed formulas]] are built freely using these connectives from a [[countable set|countably infinite]] set of [[propositional variable]]s ''p''<sub>0</sub>, ''p''<sub>1</sub>, .... A [[substitution (logic)|substitution]] ''σ'' is a function from formulas to formulas that commutes with applications of the connectives, i.e.,
:<math>\sigma f(A_1,\dots,A_n)=f(\sigma A_1,\dots,\sigma A_n)</math>
for every connective ''f'', and formulas ''A''<sub>1</sub>, ... , ''A''<sub>''n''</sub>. (We may also apply substitutions to sets Γ of formulas, making {{nowrap|1=''σ''Γ = {''σA'': ''A'' &isin; Γ}.}}) A Tarski-style [[consequence relation]]<ref>Blok & Pigozzi (1989), Kracht (2007)</ref> is a relation <math>\vdash</math> between sets of formulas, and formulas, such that
{{ordered list|start=1
|<math>A\vdash A,</math>
|if <math>\Gamma\vdash A</math> then <math>\Gamma,\Delta\vdash A,</math> ("weakening")
|if <math>\Gamma\vdash A</math> and <math>\Delta,A\vdash B</math> then <math>\Gamma,\Delta\vdash B,</math> ("composition")
}} 
for all formulas ''A'', ''B'', and sets of formulas Γ, Δ. A consequence relation such that
{{ordered list|start=4
|if <math>\Gamma\vdash A</math> then <math>\sigma\Gamma\vdash\sigma A</math>
}}
for all substitutions ''σ'' is called '''structural'''. (Note that the term "structural" as used here and below is unrelated to the notion of [[structural rule]]s in [[sequent calculus|sequent calculi]].) A structural consequence relation is called a '''propositional logic'''. A formula ''A'' is a theorem of a logic <math>\vdash</math> if <math>\varnothing\vdash A</math>.

For example, we identify a superintuitionistic logic ''L'' with its standard consequence relation <math>\vdash_L</math> generated by [[modus ponens]] and axioms, and we identify a [[normal modal logic]] with its global consequence relation <math>\vdash_L</math> generated by modus ponens, necessitation, and (as axioms) the theorems of the logic.

A '''structural inference rule'''<ref>Rybakov (1997), Def. 1.1.3</ref> (or just '''rule''' for short) is given by a pair (Γ, ''B''), usually written as
:<math>\frac{A_1,\dots,A_n}B\qquad\text{or}\qquad A_1,\dots,A_n/B,</math>
where Γ&nbsp;=&nbsp;{''A''<sub>1</sub>, ... , ''A''<sub>''n''</sub>} is a finite set of formulas, and ''B'' is a formula. An '''instance''' of the rule is
:<math>\sigma A_1,\dots,\sigma A_n/\sigma B</math>
for a substitution ''σ''. The rule Γ/''B'' is '''derivable''' in <math>\vdash</math>, if <math>\Gamma\vdash B</math>. It is '''admissible''' if for every instance of the rule, ''σB'' is a theorem whenever all formulas from ''σ''Γ are theorems.<ref>Rybakov (1997), Def. 1.7.2</ref> In other words, a rule is admissible if it, when added to the logic, does not lead to new theorems.<ref>[http://www.illc.uva.nl/D65/artemov.pdf From de Jongh’s theorem to intuitionistic logic of proofs]</ref> We also write <math>\Gamma\mathrel{|\!\!\!\sim} B</math> if Γ/''B'' is admissible. (Note that <math>\phantom{.}\!{|\!\!\!\sim}</math> 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., <math>{\vdash}={\,|\!\!\!\sim}</math>.<ref>Rybakov (1997), Def. 1.7.7</ref>

In logics with a well-behaved [[logical conjunction|conjunction]] connective (such as superintuitionistic or modal logics), a rule <math>A_1,\dots,A_n/B</math> is equivalent to <math>A_1\land\dots\land A_n/B</math> with respect to admissibility and derivability. It is therefore customary to only deal with [[unary operation|unary]] rules ''A''/''B''.