Editing Structural rule (section)

==Common structural rules==
Three common structural rules are:<ref>{{Cite journal |last=Jacobs |first=Bart |date=1994 |title=Semantics of weakening and contraction |url=https://linkinghub.elsevier.com/retrieve/pii/0168007294900205 |journal=Annals of Pure and Applied Logic |language=en |volume=69 |issue=1 |pages=73–106 |doi=10.1016/0168-0072(94)90020-5|url-access=subscription }}</ref>

* '''{{vanchor|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 [[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-->
* '''{{vanchor|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]] systems using [[Resolution (logic)|resolution]]. Known as '''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]]s; with exchange, they can be considered to be [[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]]'''.<ref name=":0" /> 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]] 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.