Three common structural rules are: • '''''', where the hypotheses or conclusion of a sequence 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 \Sigma, A} on the right. Known as
monotonicity of entailment in classical logic. • '
, where two equal (or unifiable) members on the same side of a sequent 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 in automated theorem proving systems using resolution. Known as idempotency of entailment' in classical logic. •
Exchange, where two members on the same side of a sequent 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
sequences; with exchange, they can be considered to be
multisets; and with both contraction and exchange they can be considered to be
sets. These are not the only possible structural rules. 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 (see
Curry–Howard correspondence); it often gives a good indication of the
complexity of
deciding a given logic. ==See also==