Editing Admissible rule (section)

==Variants==

A '''rule with parameters''' is a rule of the form
:<math>\frac{A(p_1,\dots,p_n,s_1,\dots,s_k)}{B(p_1,\dots,p_n,s_1,\dots,s_k)},</math>
whose variables are divided into the "regular" variables ''p''<sub>''i''</sub>, and the parameters ''s''<sub>''i''</sub>. The rule is ''L''-admissible if every ''L''-unifier ''σ'' of ''A'' such that ''σs''<sub>''i''</sub>&nbsp;=&nbsp;''s''<sub>''i''</sub> for each ''i'' is also a unifier of ''B''. The basic decidability results for admissible rules also carry to rules with parameters.<ref>Rybakov (1997), §6.1</ref>

A '''multiple-conclusion rule''' is a pair (Γ,Δ) of two finite sets of formulas, written as
:<math>\frac{A_1,\dots,A_n}{B_1,\dots,B_m}\qquad\text{or}\qquad A_1,\dots,A_n/B_1,\dots,B_m.</math>
Such a rule is admissible if every unifier of Γ is also a unifier of some formula from Δ.<ref>Jeřábek (2005); cf. Kracht (2007), §7</ref> For example, a logic ''L'' is [[consistent]] iff it admits the rule
:<math>\frac{\;\bot\;}{},</math>
and a superintuitionistic logic has the [[disjunction property]] iff it admits the rule
:<math>\frac{p\lor q}{p,q}.</math>
Again, basic results on admissible rules generalize smoothly to multiple-conclusion rules.<ref>Jeřábek (2005, 2007, 2008)</ref> 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 ''S''4 the rule above is equivalent to
:<math>\frac{A_1,\dots,A_n}{\Box B_1\lor\dots\lor\Box B_m}.</math>
Nevertheless, multiple-conclusion rules can often be employed to simplify arguments.

In [[proof theory]], admissibility is often considered in the context of [[sequent calculus|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]]
:<math>\frac{\Gamma\vdash A,\Delta\qquad\Pi,A\vdash\Lambda}{\Gamma,\Pi\vdash\Delta,\Lambda}.</math>
(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 that we obtain by translating each sequent <math>\Gamma\vdash\Delta</math> to its characteristic formula <math>\bigwedge\Gamma\to\bigvee\Delta</math>.