- Structural rule
In

proof theory , a**structural rule**is aninference rule that does not refer to any logicalconnective , but instead operates on the judgements orsequent 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 assubstructural logic s.**Common structural rules***

**Weakening**, where the hypotheses or conclusion of asequent 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 asequent 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**inautomated theorem proving systems using resolution.

***Exchange**, where two members on the same side of asequent 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

sequence s; with exchange, they aremultiset s; and with both contraction and exchange they areset s.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" (seelambda calculus ); it often gives a good indication of the complexity of deciding a given logic.**ee also***

Substructural logic

*Linear logic

*Affine logic

*Strict logic

*Ordered logic

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Structural equation modeling**— (SEM) is a statistical technique for testing and estimating causal relations using a combination of statistical data and qualitative causal assumptions. This definition of SEM was articulated by the geneticist Sewall Wright (1921),[1] the… … Wikipedia**Structural anthropology**— is based on Claude Levi Strauss s idea that people think about the world in terms of binary opposites such as high and low, inside and outside, person and animal, life and death and that every culture can be understood in terms of these opposites … Wikipedia**Structural induction**— is a proof method that is used in mathematical logic (e.g., the proof of Łoś theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction. Structural recursion is a recursion… … Wikipedia**Structural proof theory**— In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. Contents 1 Analytic proof 2 Structures and connectives 3 Cut elimination in the sequent… … Wikipedia**structural formula**— Formula For mu*la, n.; pl. E. {Formulas}, L. {Formul[ae]}. [L., dim. of forma form, model. See{Form}, n.] 1. A prescribed or set form; an established rule; a fixed or conventional method in which anything is to be done, arranged, or said. [1913… … The Collaborative International Dictionary of English**Structural Building Trades Alliance**— The Structural Building Trades Alliance (SBTA) was an American federation of labor unions in the construction industry. It was founded in 1903 and existed until 1908, when it affiliated with the American Federation of Labor (AFL) and became the… … Wikipedia**Admissible rule**— In logic, a rule of inference is admissible in a formal system if the set of theorems of the system is closed under the rule. The concept of an admissible rule was introduced by Paul Lorenzen (1955).DefinitionsThe concept of admissibility, as… … Wikipedia**Fabrication of structural steel by plasma and laser cutting**— Fabrication of dimensional (non flat) structural steel elements has historically been performed by sequential operations involving sawing, drilling and high temperature flame cutting to remove material. Each of these operations is performed on… … Wikipedia**Social rule system theory**— is an attempt to formally approach different kinds of social rule systems in a unified manner. Social rules systems include institutions such as norms, laws, regulations, taboos, customs, and a variety of related concepts and are important in the … Wikipedia**Korea under Japanese rule**— (Chōsen (Korea), Empire of Japan) 日本統治時代の朝鮮(大日本帝国朝鮮) 일제 강점기 (日帝强占期) Japanese colony … Wikipedia