In thelogical discipline ofproof theory, astructural rule is aninference rule of asequent calculus that does not refer to anylogical connective but instead operates on thesequents 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 assubstructural logics.

Three common structural rules are:^[3]

• Weakening, where the hypotheses or conclusion of a sequence may be extended with additional members. In symbolic form weakening rules can be written as${\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\Sigma }}{\mathrm{\Gamma },A⊢\mathrm{\Sigma }}}$ on the left of theturnstile, and${\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\Sigma }}{\mathrm{\Gamma }⊢\mathrm{\Sigma },A}}$ on the right. Known asmonotonicity of entailment in classical logic.
• 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:${\displaystyle \frac{\mathrm{\Gamma },A,A⊢\mathrm{\Sigma }}{\mathrm{\Gamma },A⊢\mathrm{\Sigma }}}$ and${\displaystyle \frac{\mathrm{\Gamma }⊢A,A,\mathrm{\Sigma }}{\mathrm{\Gamma }⊢A,\mathrm{\Sigma }}}$. Also known asfactoring inautomated theorem proving systems usingresolution. Known asidempotency of entailment in classical logic.
• Exchange, where two members on the same side of a sequent may be swapped. Symbolically:${\displaystyle \frac{{\mathrm{\Gamma }}_1,A,{\mathrm{\Gamma }}_2,B,{\mathrm{\Gamma }}_3⊢\mathrm{\Sigma }}{{\mathrm{\Gamma }}_1,B,{\mathrm{\Gamma }}_2,A,{\mathrm{\Gamma }}_3⊢\mathrm{\Sigma }}}$ and${\displaystyle \frac{\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_1,A,{\mathrm{\Sigma }}_2,B,{\mathrm{\Sigma }}_3}{\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_1,B,{\mathrm{\Sigma }}_2,A,{\mathrm{\Sigma }}_3}}$. (This is also known as thepermutation rule.)

A logic without any of the above structural rules would interpret the sides of a sequent as puresequences; with exchange, they can be considered to bemultisets; and with both contraction and exchange they can be considered to besets.

These are not the only possible structural rules. A famous structural rule is known ascut.^[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 ascut elimination, is directly related to the philosophy ofcomputation as normalization (seeCurry–Howard correspondence); it often gives a good indication of thecomplexity ofdeciding a given logic.

• Affine logic
• Linear logic – System of resource-aware logic
• Ordered logic (linear logic)
• Relevance logic – Kind of non-classical logic
• Separation logic – Concept in computer science

• Proof theory
• Rules of inference

• CS1 German-language sources (de)
• Articles with short description
• Short description is different from Wikidata