Structural rule

Last updated

In the logical discipline of proof theory, a structural rule is an inference rule of a sequent calculus that does not refer to any logical connective but instead operates on the sequents directly. [1] [2] 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 substructural logics.

Contents

Common structural rules

Three common structural rules are: [3]

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 . [1] 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

References

  1. 1 2 Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. I, Mathematische Zeitschrift". Mathematische Zeitschrift (in German). 39 (1): 176–210. doi:10.1007/BF01201353. ISSN   0025-5874.
  2. Szabo, M. E. (1969). Collected papers of Gerhard Gentzen. Place of publication not identified: Elsevier. ISBN   978-0-444-53419-4.
  3. Jacobs, Bart (1994). "Semantics of weakening and contraction". Annals of Pure and Applied Logic. 69 (1): 73–106. doi:10.1016/0168-0072(94)90020-5.