Structural rule

Structural rule

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

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

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

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”