In proof theory

Proof theory

Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...

, a structural rule is an inference rule that does not refer to any logical connective

Logical connective

In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...

, but instead operates on the judgements or sequent

Sequent

In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...

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

Substructural logic

In logic, a substructural logic is a logic lacking one of the usual structural rules , such as weakening, contraction or associativity...

s.

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 on the left of the turnstile
  Turnstile (symbol)
  In mathematical logic and computer science the symbol \vdash has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails"...
  
  , and 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: and . Also known as factoring in automated theorem proving
  Automated theorem proving
  Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
  
   systems using resolution
  Resolution (logic)
  In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
  
  .
• Exchange, where two members on the same side of a sequent may be swapped. Symbolically: and . (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

Sequence

In mathematics, a sequence is an ordered list of objects . Like a set, it contains members , and the number of terms is called the length of the sequence. Unlike a set, order matters, and exactly the same elements can appear multiple times at different positions in the sequence...

s; with exchange, they are multiset

Multiset

In mathematics, the notion of multiset is a generalization of the notion of set in which members are allowed to appear more than once...

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

Cut-elimination theorem

The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...

, is directly related to the philosophy of computation

Computation

Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...

 as normalization (see Curry–Howard correspondence); it often gives a good indication of the complexity

Computational complexity theory

Computational complexity theory is a branch of the theory of computation in theoretical computer science and mathematics that focuses on classifying computational problems according to their inherent difficulty, and relating those classes to each other...

 of deciding

Decision problem

In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...

 a given logic.

See also

• Substructural logic
  Substructural logic
  In logic, a substructural logic is a logic lacking one of the usual structural rules , such as weakening, contraction or associativity...
  
  
• Linear logic
  Linear logic
  Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
  
  
• Affine logic
  Affine logic
  Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening....
  
  
• Strict logic
  Strict logic
  Strict logic is essentially synonymous with relevant logic, though it can be characterized proof-theoretically as* ordinary logic without weakening, or* linear logic with contraction....
  
  
• Ordered logic