Added to Favorites

Popular Searches

Definitions

Nearby Words

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 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

## See also

- Weakening, where the hypotheses or conclusion of a sequent 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\; A,\; Sigma\}$ 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: $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.
- 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 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 lambda calculus); it often gives a good indication of the complexity of deciding a given logic.

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Wednesday June 18, 2008 at 14:34:53 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Wednesday June 18, 2008 at 14:34:53 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2015 Dictionary.com, LLC. All rights reserved.