# Structural rule

This article does not cite any references or sources. (December 2009) |

In proof theory, a **structural rule** is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as substructural logics.

## 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 on the left of the turnstile, and on the right.**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: and . Also known as**factoring**in automated theorem proving systems using resolution.**Exchange**, where two members on the same side of a sequent may be swapped. Symbolically: and . (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 are multisets; and with both contraction and exchange they are sets.

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

HPTS - Area Progetti - Edu-Soft - JavaEdu - N.Saperi - Ass.Scuola.. - TS BCTV - TS VideoRes - TSODP - TRTWE | ||