Exchange Rule

Website Links For
Structural

Information About

Exchange Rule

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 $rac{\Gamma dash \Sigma}{\Gamma, A dash \Sigma}$ on the left of the Turnstile , and $rac{\Gamma dash \Sigma}{\Gamma dash A, \Sigma}$ on the right.

Contraction, where two equal (or unifiable) members on the same side of a systems using Resolution .

Exchange, where two members on the same side of a Sequent may be swapped. Symbolically: $rac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 dash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 dash \Sigma}$ and $rac{\Gamma dash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma dash \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 are Multiset s; and with both contraction and exchange they are Set 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'' (see Lambda Calculus ); it often gives a good indication of the Complexity of Deciding a given logic.

SEE ALSO

Substructural Logic

Linear Logic

Affine Logic

Strict Logic

Ordered Logic