Admissible Rule - Variants

Variants

A rule with parameters is a rule of the form

whose variables are divided into the "regular" variables p_i, and the parameters s_i. The rule is L-admissible if every L-unifier σ of A such that σs_i = s_i for each i is also a unifier of B. The basic decidability results for admissible rules also carry to rules with parameters.

A multiple-conclusion rule is a pair (Γ,Δ) of two finite sets of formulas, written as

Such a rule is admissible if every unifier of Γ is also a unifier of some formula from Δ. For example, a logic L is consistent iff it admits the rule

and a superintuitionistic logic has the disjunction property iff it admits the rule

Again, basic results on admissible rules generalize smoothly to multiple-conclusion rules. In logics with a variant of the disjunction property, the multiple-conclusion rules have the same expressive power as single-conclusion rules: for example, in S4 the rule above is equivalent to

Nevertheless, multiple-conclusion rules can often be employed to simplify arguments.

In proof theory, admissibility is often considered in the context of sequent calculi, where the basic objects are sequents rather than formulas. For example, one can rephrase the cut-elimination theorem as saying that the cut-free sequent calculus admits the cut rule

(By abuse of language, it is also sometimes said that the (full) sequent calculus admits cut, meaning its cut-free version does.) However, admissibility in sequent calculi is usually only a notational variant for admissibility in the corresponding logic: any complete calculus for (say) intuitionistic logic admits a sequent rule if and only if IPC admits the formula rule which we obtain by translating each sequent to its characteristic formula .