View source for Structural rule

{{Short description|Rule of mathematical logic}}
In the logical discipline of [[Proof theory|proof theory]], a '''structural rule''' is an inference rule of a [[Sequent calculus|sequent calculus]] that does not refer to any [[Logical connective|logical connective]] but instead operates on the [[Sequent|sequent]]s directly. Structural rules often mimic the intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as [[Philosophy:Substructural logic|substructural logic]]s.

==Common structural rules==
Three common structural rules are:

* {{Anchor|Weakening}}'''Weakening''', where the hypotheses or conclusion of a sequence may be extended with additional members. In symbolic form weakening rules can be written as <math>\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> on the left of the [[Turnstile (symbol)|turnstile]], and <math>\frac{\Gamma \vdash \Sigma}{\Gamma \vdash \Sigma, A}</math> on the right. Known as [[Philosophy:Monotonicity of entailment|monotonicity of entailment]] in classical logic.
<!--N.B. the A on the bottom *is* the correct way around for the right weakening rule; see the talk page-->
* '''Contraction''', where two equal (or unifiable) members on the same side of a sequent may be replaced by a single member (or common instance). Symbolically: <math>\frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}</math>. Also known as '''factoring''' in [[Automated theorem proving|automated theorem proving]] systems using [[Philosophy:Resolution (logic)|resolution]]. Known as [[Philosophy:Idempotency of entailment|idempotency of entailment]] in classical logic.
* '''Exchange''', where two members on the same side of a sequent may be swapped. Symbolically: <math>\frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}</math>. (This is also known as the ''permutation rule''.)

A logic without any of the above structural rules would interpret the sides of a sequent as pure [[Sequence|sequence]]s; with exchange, they can be considered to be [[Multiset|multiset]]s; and with both contraction and exchange they can be considered to be [[Set (mathematics)|set]]s.

These are not the only possible structural rules. A famous structural rule is known as '''[[Cut rule|cut]]'''. Considerable effort is spent by proof theorists in showing that cut rules are superfluous in various logics. More precisely, what is shown is that cut is only (in a sense) a tool for abbreviating proofs, and does not add to the theorems that can be proved. The successful 'removal' of cut rules, known as ''[[Cut-elimination theorem|cut elimination]]'', is directly related to the philosophy of ''[[Computation|computation]] as normalization'' (see [[Curry–Howard correspondence]]); it often gives a good indication of the [[Computational complexity theory|complexity]] of [[Decision problem|deciding]] a given logic.

==See also==
*{{annotated link|Philosophy:Affine logic}}
*{{annotated link|Linear logic}}
*{{annotated link|Philosophy:Relevance logic}}
*{{annotated link|Separation logic}}

{{Non-classical logic}}

[[Category:Proof theory]]
[[Category:Rules of inference]]

{{Sourceattribution|Structural rule}}