Structural rule: Difference between revisions

Content deleted Content added

Inline

Latest revision as of 10:34, 28 April 2024

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.

Common structural rules

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 ${\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.
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: ${\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.^[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.

References

^ ^a ^b 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.
^ Szabo, M. E. (1969). Collected papers of Gerhard Gentzen. Place of publication not identified: Elsevier. ISBN 978-0-444-53419-4.
^ 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.

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

[1]

[2]

[3]

@@ Line 1: / Line 1: @@
+{{Short description|Rule of mathematical logic}}
-In [[proof theory]], a '''structural rule''' is an [[inference rule]] that does not refer to any logical [[connective]], but instead operates on the judgements or [[sequent]]s 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 logic]]s.
+{{for|the type of rule used in linguistics|phrase structure rule}}
+In the [[formal logic|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 [[sequent]]s directly.<ref name=":0">{{Cite journal |last=Gentzen |first=Gerhard |date=1935 |title=Untersuchungen über das logische Schließen. I, Mathematische Zeitschrift |url=http://link.springer.com/10.1007/BF01201353 |journal=Mathematische Zeitschrift |language=de |volume=39 |issue=1 |pages=176–210 |doi=10.1007/BF01201353 |issn=0025-5874}}</ref><ref>{{Cite book |last=Szabo |first=M. E. |title=Collected papers of Gerhard Gentzen |date=1969 |publisher=Elsevier |isbn=978-0-444-53419-4 |location=Place of publication not identified}}</ref> 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 logic]]s.
 ==Common structural rules==
+Three common structural rules are:<ref>{{Cite journal |last=Jacobs |first=Bart |date=1994 |title=Semantics of weakening and contraction |url=https://linkinghub.elsevier.com/retrieve/pii/0168007294900205 |journal=Annals of Pure and Applied Logic |language=en |volume=69 |issue=1 |pages=73–106 |doi=10.1016/0168-0072(94)90020-5}}</ref>
-* '''Weakening''', where the hypotheses or conclusion of a [[sequent]] may be extended with additional members. In symbolic form weakening rules can be written as <math>\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> on the left of the [[turnstile]], and <math>\frac{\Gamma \vdash A, \Sigma}{\Gamma \vdash \Sigma}</math> 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: <math>\frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}</math>. Also known as '''factoring''' in [[automated theorem proving]] systems using [[Resolution (logic)|resolution]].
-* '''Exchange''', where two members on the same side of a [[sequent]] may be swapped. Symbolically: <math>\frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}</math>. (This is also known as the ''permutation rule''.)
+* {{Anchor|Weakening}}'''Weakening''', where the hypotheses or conclusion of a sequence may be extended with additional members. In symbolic form weakening rules can be written as <math>\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> on the left of the [[Turnstile (symbol)|turnstile]], and <math>\frac{\Gamma \vdash \Sigma}{\Gamma \vdash \Sigma, A}</math> on the right. Known as [[monotonicity of entailment]] in classical logic.
-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.
+<!--N.B. the A on the bottom *is* the correct way around for the right weakening rule; see the talk page-->
+* '''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: <math>\frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}</math>. Also known as '''factoring''' in [[automated theorem proving]] systems using [[Resolution (logic)|resolution]]. Known as [[idempotency of entailment]] in classical logic.
+* '''Exchange''', where two members on the same side of a sequent may be swapped. Symbolically: <math>\frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma}</math> and <math>\frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}</math>. (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 can be considered to be [[multiset]]s; and with both contraction and exchange they can be considered to be [[set (mathematics)|set]]s.
-A famous structural rule is known as '''[[cut rule|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 theorem|cut elimination]]'', is directly related to the philosophy of ''[[computation]] as normalization'' (see [[lambda calculus]]); it often gives a good indication of the [[complexity theory|complexity]] of [[decision problem|deciding]] a given logic.
+These are not the only possible structural rules. A famous structural rule is known as '''[[cut rule|cut]]'''.<ref name=":0" /> 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 theorem|cut elimination]]'', is directly related to the philosophy of ''[[computation]] as normalization'' (see [[Curry–Howard correspondence]]); it often gives a good indication of the [[computational complexity theory|complexity]] of [[decision problem|deciding]] a given logic.
 ==See also==
-*[[Substructural logic]]
+*{{annotated link|Affine logic}}
-*[[Linear logic]]
+*{{annotated link|Linear logic}}
+*{{annotated link|Ordered logic (linear logic)}}
-*[[Affine logic]]
+*{{annotated link|Relevance logic}}
-*[[Strict logic]]
+*{{annotated link|Separation logic}}
-*[[Ordered logic]]
+==References==
-[[Category:Proof theory]]
+{{Reflist}}
+{{Non-classical logic}}
-[[zh:结构规则]]
+[[Category:Proof theory]]
+[[Category:Rules of inference]]

v t e Non-classical logic
Intuitionistic	Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory
Fuzzy	Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations
Substructural	Structural rule Relevance logic Linear logic
Paraconsistent	Dialetheism
Description	Ontology (computer science) Ontology language
Many-valued	Three-valued Four-valued Łukasiewicz
Digital logic	Three-state logic Tri-state buffer Four-valued Verilog IEEE 1164 VHDL
Others	Dynamic semantics Inquisitive logic Intermediate logic Non-monotonic logic