1 Definition and basic idea

Contraction is a structural rule in logic that permits two identical occurrences of a formula to be replaced by one. It expresses the idea that duplication of the same assumption does not increase what can be derived in a proof system. The rule is most familiar in sequent calculus, where formulas are arranged in contexts and may be manipulated by structural principles.

1.1 Informal explanation

If a derivation uses the same premise twice, contraction allows those two copies to be treated as a single copy. In everyday terms, it says that “having it twice” is no stronger than “having it once” when the repeated item is exactly the same formula. This makes contraction a formal counterpart to the intuitive idea that duplicate information can often be consolidated without changing the outcome.

1.2 Formal statement

In proof systems that include contraction, the rule is usually stated as an inference from a context containing repeated formulas to a context containing one fewer copy. The exact presentation depends on whether formulas occur on the left or right side of a sequent, and on the conventions of the calculus being used.

1.2.1 Contraction on the left

In a sequent calculus, left contraction typically has the form:

\[ \Gamma, A, A \vdash \Delta \;\Rightarrow\; \Gamma, A \vdash \Delta \]

It says that if a sequent is derivable with two copies of \(A\) among the assumptions, then one of those copies may be removed. This is the most common version in classical and intuitionistic sequent systems.

1.2.2 Contraction on the right

Some systems also admit a right-sided version, especially in formalisms where formulas may appear symmetrically on both sides or where the right side is treated as a multiset of conclusions. In such settings, the analogous rule reduces repeated occurrences on the right:

\[ \Gamma \vdash A, A, \Delta \;\Rightarrow\; \Gamma \vdash A, \Delta \]

Whether this is meaningful depends on the specific logic and its sequent conventions.

1.3 Notation and proof-rule form

Contraction is often written as a rule schema rather than a single concrete inference. The most familiar notation marks the repeated formula with a brace or repeated entry in the context. Because contexts are usually understood as multisets or sequences, the rule can be presented either as elimination of an extra copy or as a transformation of a proof tree. In many expositions, contraction is grouped with weakening and exchange as a structural rule, since it changes the shape of assumptions rather than the internal logical content of formulas.

2 Contraction in proof theory

Contraction plays an important role in proof theory because it governs how assumptions may be reused. Its presence or absence has significant consequences for proof search, normalization, and the overall expressive behavior of a formal system.

2.1 Role in sequent calculus

In sequent calculus, contraction helps control the multiplicity of assumptions in a derivation. It allows a proof to simplify contexts that contain repeated formulas, which is especially useful in systems where rules may introduce the same formula more than once. Because sequents are often manipulated by structural transformations, contraction is a standard tool for keeping derivations manageable.

2.1.1 Structural rules

Structural rules describe how the surrounding context of a proof may change independently of the logical connectives. Contraction belongs to this family, together with weakening and exchange. These rules do not introduce new logical content; instead, they regulate the use, omission, and ordering of existing formulas in a derivation.

2.1.1.1 Comparison with weakening and exchange

Weakening permits extra unused formulas to be added, exchange permits the order of formulas to be rearranged, and contraction permits duplicates to be merged. Together, these three rules determine much of the behavior of contexts in classical-style proof systems. Among them, contraction is the one most directly tied to duplication and reuse of assumptions.

2.2 Admissibility and derivability

In some proof systems, contraction is not a primitive rule but is instead admissible. This means that although the rule is not stated as a basic inference, any proof that seems to require it can be transformed into one that does not rely on it explicitly. In other systems, contraction is derivable from other rules or built into the underlying semantics of the logic.

2.3 Cut-free proofs and normalization

Contraction interacts in subtle ways with cut elimination and proof normalization. In cut-free settings, the treatment of repeated assumptions can affect the complexity of derivations and the size of proof trees. Proof transformations may duplicate or merge subproofs, so contraction often appears in analyses of how proofs can be simplified while preserving derivability. Its presence can make some derivations shorter, but it may also obscure resource sensitivity in systems designed to track exact usage.

3 Logical interpretations

Contraction has several interpretive readings, depending on the philosophical or semantic perspective adopted for a logic. It is often discussed as a principle about resources, reuse, or the structural shape of inference.

3.1 Resource-based reading

From a resource perspective, contraction says that a resource can be copied without loss. In logics where formulas represent consumable resources, this is a strong principle because it permits unrestricted reuse of an item that may otherwise be treated as single-use. Systems that reject contraction often do so precisely to prevent this kind of unrestricted duplication.

3.2 Structural significance

Contraction is significant because it reveals that a logic treats contexts as insensitive to multiplicity, at least for the formulas to which the rule applies. This makes the proof system less concerned with counting occurrences and more concerned with whether a formula is present at all. In that sense, contraction marks a move from linear resource accounting toward classical-style inferential behavior.

3.3 Relation to duplication of assumptions

At the level of assumptions, contraction formalizes the intuition that repeating an identical hypothesis does not create a stronger premise set. If a conclusion follows from one occurrence of a premise, it should also follow from two identical occurrences, and vice versa in systems where contraction is available. This principle underlies many standard proof manipulations in ordinary logic.

4 Contraction in substructural logics

Substructural logics are defined in part by limiting or omitting structural rules such as contraction. These systems explore alternative notions of implication, inference, and resource use by controlling how assumptions may be duplicated, discarded, or rearranged.

4.1 Linear logic

Linear logic is the best-known setting in which contraction is restricted. In its core fragment, formulas are treated as resources that must be used with care, so unrestricted duplication is not permitted. The logic distinguishes between formulas that may be copied and those that may not, making contraction a carefully controlled rather than universal principle.

4.2 Relevant logic

Relevant logic seeks to ensure that premises are meaningfully connected to conclusions. For that reason, it often resists structural principles that would allow arbitrary reuse of assumptions. Limiting contraction helps preserve the relevance of premises by preventing proofs from relying on repeated or disconnected copies of the same formula.

4.3 Affine logic

Affine logic is a weaker resource-sensitive system in which weakening is allowed but contraction is not generally available. This means that a formula may be discarded, but not duplicated. As a result, affine logic occupies an intermediate position between classical logic and fully linear systems.

4.4 Logics without contraction

Logics without contraction emphasize the distinct contribution of each assumption. Their proof theory is sensitive to multiplicity, so a formula occurring twice may genuinely differ from one occurring once. Such systems are useful for modeling finite resources, protocols, and situations where duplication is not automatically legitimate.

5 Variants and extensions

Contraction can be formulated in different ways depending on the structure of the proof system and the needs of the application. Some variants control how many copies may be merged, while others restrict the rule to certain formulas or contexts.

5.1 Multiple contraction

Multiple contraction allows more than two identical occurrences to be reduced at once. Instead of removing a single duplicate step by step, the rule may collapse several copies into one in a single inference. This is mostly a matter of presentation, since repeated ordinary contractions often achieve the same effect.

5.2 Restricted contraction

Restricted contraction applies only to designated formulas or classes of formulas. For example, a system may allow duplication for persistent propositions but not for linear resources. Such restrictions are common in logics that distinguish between reusable and non-reusable assumptions.

5.3 Context-sensitive formulations

Some proof systems formulate contraction in a context-sensitive way, so that its applicability depends on where a formula appears or on additional annotations attached to the context. These formulations are useful in specialized calculi where the ordinary notion of a plain formula occurrence is too coarse to capture the intended inferential behavior.

6 Examples

Examples of contraction show how duplicate assumptions can be eliminated in practice and how proofs can be reorganized to make their use explicit or redundant.

6.1 Simple derivations using contraction

Suppose a derivation produces a sequent with two identical assumptions \(P, P\). If the same conclusion can be obtained from one \(P\), contraction allows the proof to replace the duplicate pair with a single occurrence. This makes the context shorter without altering the derivability of the sequent.

6.2 Proof transformations

In proof transformations, contraction may appear when a rule introduces the same formula in separate branches of a derivation. A later contraction step can merge those copies, simplifying the surrounding context. Such transformations are common in the study of normalization and cut elimination, where one aims to reorganize proofs without changing their conclusions.

6.3 Eliminating duplicate hypotheses

A common use of contraction is to remove redundant hypotheses from a proof. If a theorem is established under assumptions \(A\) and \(A\) together, contraction shows that the second copy does not contribute additional inferential power. The result is a cleaner derivation with a leaner assumption set.

Contraction is closely linked to other structural rules and to algebraic ideas that capture redundancy and repetition. These connections help explain its role across logic and semantics.

7.1 Weakening

Weakening allows extra formulas to be added to a context without affecting derivability. Together with contraction, it governs whether a logic is insensitive to unused or repeated assumptions. Weakening concerns omission, while contraction concerns duplication.

7.2 Exchange

Exchange permits the reordering of formulas in a context. It is often listed alongside contraction because both are structural rules that modify the arrangement of assumptions rather than their logical content. Exchange changes order; contraction changes multiplicity.

7.3 Idempotence in algebraic semantics

In algebraic semantics, contraction is often associated with idempotence-like behavior, where combining a proposition with itself yields no new information. This helps connect proof-theoretic contraction with algebraic structures in which repeated elements collapse to a single effective instance.

</INTERNAL_LINK_CANDIDATES> Structural rule (a rule governing the form of assumptions in proofs) Sequent calculus (a proof formalism using sequents and inference rules) Weakening (a structural rule that permits adding unused assumptions) Exchange (a structural rule that permits reordering assumptions) Cut elimination (a normalization process removing cut inferences) Normalization (a process simplifying proofs to canonical form) Admissibility (a property of a rule that can be eliminated from derivations) Derivability (the property of being provable within a system) Linear logic (a resource-sensitive logic with restricted contraction) Relevant logic (a logic requiring relevance between premises and conclusions) Affine logic (a logic allowing weakening but restricting contraction) Substructural logic (a family of logics limiting structural rules) Resource semantics (an interpretation of formulas as consumable resources) Proof transformation (a method of converting one proof into another) Hypothesis (an assumption used in a derivation) Context (the surrounding list or multiset of formulas in a sequent) Multiset (an unordered collection where repeated elements count separately) Idempotence (a property where combining something with itself changes nothing) Classical logic (a logic that typically permits contraction freely) Intuitionistic logic (a logic often presented with contraction in sequent form)