Admissible Rule - Definitions

Definitions

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, in the case of superintuitionistic logics, or in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p_n. A substitution σ is a function from formulas to formulas which commutes with the connectives, i.e.,

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 is a relation between sets of formulas, and formulas, such that

1. if then
2. if and then

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

4. if then

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 if .

For example, we identify a superintuitionistic logic L with its standard consequence relation axiomatizable by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation axiomatized by modus ponens, necessitation, and axioms.

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

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

for a substitution σ. The rule Γ/B is derivable in, if . It is admissible if for every instance of the rule, σB is a theorem whenever all formulas from σΓ are theorems. In other words, a rule is admissible if, when added to the logic, does not lead to new theorems. We also write if Γ/B is admissible. (Note that 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., .

In logics with a well-behaved conjunction connective (such as superintuitionistic or modal logics), a rule is equivalent to with respect to admissibility and derivability. It is therefore customary to only deal with unary rules A/B.