- Structural rule
In
proof theory , a structural rule is aninference rule that does not refer to any logicalconnective , but instead operates on the judgements orsequent s directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified assubstructural logic s.Common structural rules
* Weakening, where the hypotheses or conclusion of a
sequent may be extended with additional members. In symbolic form weakening rules can be written as frac{Gamma vdash Sigma}{Gamma, A vdash Sigma} on the left of the turnstile, and frac{Gamma vdash Sigma}{Gamma vdash A, Sigma} on the right.
* Contraction, where two equal (or unifiable) members on the same side of asequent may be replaced by a single member (or common instance). Symbolically: frac{Gamma, A, A vdash Sigma}{Gamma, A vdash Sigma} and frac{Gamma vdash A, A, Sigma}{Gamma vdash A, Sigma}. Also known as factoring inautomated theorem proving systems using resolution.
* Exchange, where two members on the same side of asequent may be swapped. Symbolically: frac{Gamma_1, A, Gamma_2, B, Gamma_3 vdash Sigma}{Gamma_1, B, Gamma_2, A, Gamma_3 vdash Sigma} and frac{Gamma vdash Sigma_1, A, Sigma_2, B, Sigma_3}{Gamma vdash Sigma_1, B, Sigma_2, A, Sigma_3}. (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 s; with exchange, they aremultiset s; and with both contraction and exchange they areset s.A famous structural rule is known as 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", is directly related to the philosophy of "
computation as normalization" (seelambda calculus ); it often gives a good indication of the complexity of deciding a given logic.ee also
*
Substructural logic
*Linear logic
*Affine logic
*Strict logic
*Ordered logic
Wikimedia Foundation. 2010.