Sequent calculus

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Variations: Mix)
(Equivalence: Link to List of equivalences)
 
(One intermediate revision by one user not shown)
Line 453: Line 453:
 
Any pair of connectives that has the same rules as <math>\tens/\parr</math> is
 
Any pair of connectives that has the same rules as <math>\tens/\parr</math> is
 
equivalent to it, the same holds for additives, but not for exponentials.
 
equivalent to it, the same holds for additives, but not for exponentials.
  +
  +
Other [[List of equivalences|basic equivalences]] exist.
   
 
== Properties of proofs ==
 
== Properties of proofs ==
Line 625: Line 627:
 
cuts, since in the case of <math>\with</math> we duplicated a part of the
 
cuts, since in the case of <math>\with</math> we duplicated a part of the
 
original proof.}}
 
original proof.}}
  +
  +
A corresponding property for positive connectives is [[Reversibility and focalization|focalization]], which states that clusters of positive formulas can be treated in one step, under certain circumstances.
   
 
== One-sided sequent calculus ==
 
== One-sided sequent calculus ==

Latest revision as of 15:46, 28 October 2013

This article presents the language and sequent calculus of second-order linear logic and the basic properties of this sequent calculus. The core of the article uses the two-sided system with negation as a proper connective; the one-sided system, often used as the definition of linear logic, is presented at the end of the page.

Contents

[edit] Formulas

Atomic formulas, written α,β,γ, are predicates of the form p(t_1,\ldots,t_n), where the ti are terms from some first-order language. The predicate symbol p may be either a predicate constant or a second-order variable. By convention we will write first-order variables as x,y,z, second-order variables as X,Y,Z, and ξ for a variable of arbitrary order (see Notations).

Formulas, represented by capital letters A, B, C, are built using the following connectives:

α atom A\orth negation
A \tens B tensor A \parr B par multiplicatives
\one one \bot bottom multiplicative units
A \plus B plus A \with B with additives
\zero zero \top top additive units
\oc A of course \wn A why not exponentials
\exists \xi.A there exists \forall \xi.A for all quantifiers

Each line (except the first one) corresponds to a particular class of connectives, and each class consists in a pair of connectives. Those in the left column are called positive and those in the right column are called negative. The tensor and with connectives are conjunctions while par and plus are disjunctions. The exponential connectives are called modalities, and traditionally read of course A for \oc A and why not A for \wn A. Quantifiers may apply to first- or second-order variables.

There is no connective for implication in the syntax of standard linear logic. Instead, a linear implication is defined similarly to the decomposition A\imp B=\neg A\vee B in classical logic, as A\limp B:=A\orth\parr B.

Free and bound variables and first-order substitution are defined in the standard way. Formulas are always considered up to renaming of bound names. If A is a formula, X is a second-order variable and B[x_1,\ldots,x_n] is a formula with variables xi, then the formula A[B / X] is A where every atom X(t_1,\ldots,t_n) is replaced by B[t_1,\ldots,t_n].

[edit] Sequents and proofs

A sequent is an expression \Gamma\vdash\Delta where Γ and Δ are finite multisets of formulas. For a multiset \Gamma=A_1,\ldots,A_n, the notation \wn\Gamma represents the multiset \wn A_1,\ldots,\wn A_n. Proofs are labelled trees of sequents, built using the following inference rules:

  • Identity group: 
\LabelRule{\rulename{axiom}}
\NulRule{ A \vdash A }
\DisplayProof

\AxRule{ \Gamma \vdash A, \Delta }
\AxRule{ \Gamma', A \vdash \Delta' }
\LabelRule{\rulename{cut}}
\BinRule{ \Gamma, \Gamma' \vdash \Delta, \Delta' }
\DisplayProof
  • Negation: 
\AxRule{ \Gamma \vdash A, \Delta }
\UnaRule{ \Gamma, A\orth \vdash \Delta }
\LabelRule{n_L}
\DisplayProof

\AxRule{ \Gamma, A \vdash \Delta }
\UnaRule{ \Gamma \vdash A\orth, \Delta }
\LabelRule{n_R}
\DisplayProof
  • Multiplicative group:
    • tensor: 
\AxRule{ \Gamma, A, B \vdash \Delta }
\LabelRule{ \tens_L }
\UnaRule{ \Gamma, A \tens B \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash A, \Delta }
\AxRule{ \Gamma' \vdash B, \Delta' }
\LabelRule{ \tens_R }
\BinRule{ \Gamma, \Gamma' \vdash A \tens B, \Delta, \Delta' }
\DisplayProof
    • par: 
\AxRule{ \Gamma, A \vdash \Delta }
\AxRule{ \Gamma', B \vdash \Delta' }
\LabelRule{ \parr_L }
\BinRule{ \Gamma, \Gamma', A \parr B \vdash \Delta, \Delta' }
\DisplayProof

\AxRule{ \Gamma \vdash A, B, \Delta }
\LabelRule{ \parr_R }
\UnaRule{ \Gamma \vdash A \parr B, \Delta }
\DisplayProof
    • one: 
\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ \one_L }
\UnaRule{ \Gamma, \one \vdash \Delta }
\DisplayProof

\LabelRule{ \one_R }
\NulRule{ \vdash \one }
\DisplayProof
    • bottom: 
\LabelRule{ \bot_L }
\NulRule{ \bot \vdash }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ \bot_R }
\UnaRule{ \Gamma \vdash \bot, \Delta }
\DisplayProof
  • Additive group:
    • plus: 
\AxRule{ \Gamma, A \vdash \Delta }
\AxRule{ \Gamma, B \vdash \Delta }
\LabelRule{ \plus_L }
\BinRule{ \Gamma, A \plus B \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash A, \Delta }
\LabelRule{ \plus_{R1} }
\UnaRule{ \Gamma \vdash A \plus B, \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash B, \Delta }
\LabelRule{ \plus_{R2} }
\UnaRule{ \Gamma \vdash A \plus B, \Delta }
\DisplayProof
    • with: 
\AxRule{ \Gamma, A \vdash \Delta }
\LabelRule{ \with_{L1} }
\UnaRule{ \Gamma, A \with B \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma, B \vdash \Delta }
\LabelRule{ \with_{L2} }
\UnaRule{ \Gamma, A \with B \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash A, \Delta }
\AxRule{ \Gamma \vdash B, \Delta }
\LabelRule{ \with_R }
\BinRule{ \Gamma \vdash A \with B, \Delta }
\DisplayProof
    • zero: 
\LabelRule{ \zero_L }
\NulRule{ \Gamma, \zero \vdash \Delta }
\DisplayProof
    • top: 
\LabelRule{ \top_R }
\NulRule{ \Gamma \vdash \top, \Delta }
\DisplayProof
  • Exponential group:
    • of course: 
\AxRule{ \Gamma, A \vdash \Delta }
\LabelRule{ d_L }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ w_L }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma, \oc A, \oc A \vdash \Delta }
\LabelRule{ c_L }
\UnaRule{ \Gamma, \oc A \vdash \Delta }
\DisplayProof

\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B ,\wn B_1, \ldots, \wn B_m }
\LabelRule{ \oc_R }
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B ,\wn B_1, \ldots, \wn B_m }
\DisplayProof
    • why not: 
\AxRule{ \Gamma \vdash A, \Delta }
\LabelRule{ d_R }
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta }
\LabelRule{ w_R }
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \wn A, \wn A, \Delta }
\LabelRule{ c_R }
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof

\AxRule{ \oc A_1, \ldots, \oc A_n, A \vdash \wn B_1, \ldots, \wn B_m }
\LabelRule{ \wn_L }
\UnaRule{ \oc A_1, \ldots, \oc A_n, \wn A \vdash \wn B_1, \ldots, \wn B_m }
\DisplayProof
  • Quantifier group (in the \exists_L and \forall_R rules, ξ must not occur free in Γ or Δ):
    • there exists: 
\AxRule{ \Gamma , A \vdash \Delta }
\LabelRule{ \exists_L }
\UnaRule{ \Gamma, \exists\xi.A \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta, A[t/x] }
\LabelRule{ \exists^1_R }
\UnaRule{ \Gamma \vdash \Delta, \exists x.A }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta, A[B/X] }
\LabelRule{ \exists^2_R }
\UnaRule{ \Gamma \vdash \Delta, \exists X.A }
\DisplayProof
    • for all: 
\AxRule{ \Gamma, A[t/x] \vdash \Delta }
\LabelRule{ \forall^1_L }
\UnaRule{ \Gamma, \forall x.A \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma, A[B/X] \vdash \Delta }
\LabelRule{ \forall^2_L }
\UnaRule{ \Gamma, \forall X.A \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta, A }
\LabelRule{ \forall_R }
\UnaRule{ \Gamma \vdash \Delta, \forall\xi.A }
\DisplayProof

The left rules for of course and right rules for why not are called dereliction, weakening and contraction rules. The right rule for of course and the left rule for why not are called promotion rules. Note the fundamental fact that there are no contraction and weakening rules for arbitrary formulas, but only for the formulas starting with the \wn modality. This is what distinguishes linear logic from classical logic: if weakening and contraction were allowed for arbitrary formulas, then \tens and \with would be identified, as well as \plus and \parr, \one and \top, \zero and \bot. By identified, we mean here that replacing a \tens with a \with or vice versa would preserve provability.

Sequents are considered as multisets, in other words as sequences up to permutation. An alternative presentation would be to define a sequent as a finite sequence of formulas and to add the exchange rules:


\AxRule{ \Gamma_1, A, B, \Gamma_2 \vdash \Delta }
\LabelRule{\rulename{exchange}_L}
\UnaRule{ \Gamma_1, B, A, \Gamma_2 \vdash \Delta }
\DisplayProof

\AxRule{ \Gamma \vdash \Delta_1, A, B, \Delta_2 }
\LabelRule{\rulename{exchange}_R}
\UnaRule{ \Gamma \vdash \Delta_1, B, A, \Delta_2 }
\DisplayProof

[edit] Equivalences

Two formulas A and B are (linearly) equivalent, written A\linequiv B, if both implications A\limp B and B\limp A are provable. Equivalently, A\linequiv B if both A\vdash B and B\vdash A are provable. Another formulation of A\linequiv B is that, for all Γ and Δ, \Gamma\vdash\Delta,A is provable if and only if \Gamma\vdash\Delta,B is provable.

Two related notions are isomorphism (stronger than equivalence) and equiprovability (weaker than equivalence).

[edit] De Morgan laws

Negation is involutive:

A\linequiv A\biorth

Duality between connectives:

 ( A \tens B )\orth \linequiv A\orth \parr B\orth  ( A \parr B )\orth \linequiv A\orth \tens B\orth
 \one\orth \linequiv \bot  \bot\orth \linequiv \one
 ( A \plus B )\orth \linequiv A\orth \with B\orth  ( A \with B )\orth \linequiv A\orth \plus B\orth
 \zero\orth \linequiv \top  \top\orth \linequiv \zero
 ( \oc A )\orth \linequiv \wn ( A\orth )  ( \wn A )\orth \linequiv \oc ( A\orth )
 ( \exists \xi.A )\orth \linequiv \forall \xi.( A\orth )  ( \forall \xi.A )\orth \linequiv \exists \xi.( A\orth )

[edit] Fundamental equivalences

  • Associativity, commutativity, neutrality:
    
A \tens (B \tens C) \linequiv (A \tens B) \tens C 
A \tens B \linequiv B \tens A 
A \tens \one \linequiv A
    
A \parr (B \parr C) \linequiv (A \parr B) \parr C 
A \parr B \linequiv B \parr A 
A \parr \bot \linequiv A
    
A \plus (B \plus C) \linequiv (A \plus B) \plus C 
A \plus B \linequiv B \plus A 
A \plus \zero \linequiv A
    
A \with (B \with C) \linequiv (A \with B) \with C 
A \with B \linequiv B \with A 
A \with \top \linequiv A
  • Idempotence of additives:
    
A \plus A \linequiv A 
A \with A \linequiv A
  • Distributivity of multiplicatives over additives:
    
A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) 
A \tens \zero \linequiv \zero
    
A \parr (B \with C) \linequiv (A \parr B) \with (A \parr C) 
A \parr \top \linequiv \top
  • Defining property of exponentials:
    
\oc(A \with B) \linequiv \oc A \tens \oc B 
\oc\top \linequiv \one
    
\wn(A \plus B) \linequiv \wn A \parr \wn B 
\wn\zero \linequiv \bot
  • Monoidal structure of exponentials:
    
\oc A \tens \oc A \linequiv \oc A 
\oc \one \linequiv \one
    
\wn A \parr \wn A \linequiv \wn A 
\wn \bot \linequiv \bot
  • Digging:
    
\oc\oc A \linequiv \oc A 
\wn\wn A \linequiv \wn A
  • Other properties of exponentials:
    
\oc\wn\oc\wn A \linequiv \oc\wn A 
\oc\wn \one \linequiv \one
    
\wn\oc\wn\oc A \linequiv \wn\oc A 
\wn\oc \bot \linequiv \bot

These properties of exponentials lead to the lattice of exponential modalities.

  • Commutation of quantifiers (ζ does not occur in A):
    
\exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A 
\exists \xi.(A \plus B) \linequiv \exists \xi.A \plus \exists \xi.B 
\exists \zeta.(A\tens B) \linequiv A\tens\exists \zeta.B 
\exists \zeta.A \linequiv A
    
\forall \xi. \forall \psi. A \linequiv \forall \psi. \forall \xi. A 
\forall \xi.(A \with B) \linequiv \forall \xi.A \with \forall \xi.B 
\forall \zeta.(A\parr B) \linequiv A\parr\forall \zeta.B 
\forall \zeta.A \linequiv A

[edit] Definability

The units and the additive connectives can be defined using second-order quantification and exponentials, indeed the following equivalences hold:

  •  \zero \linequiv \forall X.X
  •  \one \linequiv \forall X.(X \limp X)
  •  A \plus B \linequiv \forall X.(\oc(A \limp X) \limp \oc(B \limp X) \limp X)

The constants \top and \bot and the connective \with can be defined by duality.

Any pair of connectives that has the same rules as \tens/\parr is equivalent to it, the same holds for additives, but not for exponentials.

Other basic equivalences exist.

[edit] Properties of proofs

[edit] Cut elimination and consequences

Theorem (cut elimination)

For every sequent \Gamma\vdash\Delta, there is a proof of \Gamma\vdash\Delta if and only if there is a proof of \Gamma\vdash\Delta that does not use the cut rule.

This property is proved using a set of rewriting rules on proofs, using appropriate termination arguments (see the specific articles on cut elimination for detailed proofs), it is the core of the proof/program correspondence.

It has several important consequences:

Definition (subformula)

The subformulas of a formula A are A and, inductively, the subformulas of its immediate subformulas:

  • the immediate subformulas of A\tens B, A\parr B, A\plus B, A\with B are A and B,
  • the only immediate subformula of \oc A and \wn A is A,
  • \one, \bot, \zero, \top and atomic formulas have no immediate subformula,
  • the immediate subformulas of \exists x.A and \forall x.A are all the A[t / x] for all first-order terms t,
  • the immediate subformulas of \exists X.A and \forall X.A are all the A[B / X] for all formulas B (with the appropriate number of parameters).

Theorem (subformula property)

A sequent \Gamma\vdash\Delta is provable if and only if it is the conclusion of a proof in which each intermediate conclusion is made of subformulas of the formulas of Γ and Δ.

Proof. By the cut elimination theorem, if a sequent is provable, then it is provable by a cut-free proof. In each rule except the cut rule, all formulas of the premisses are either formulas of the conclusion, or immediate subformulas of it, therefore cut-free proofs have the subformula property.

The subformula property means essentially nothing in the second-order system, since any formula is a subformula of a quantified formula where the quantified variable occurs. However, the property is very meaningful if the sequent Γ does not use second-order quantification, as it puts a strong restriction on the set of potential proofs of a given sequent. In particular, it implies that the first-order fragment without quantifiers is decidable.

Theorem (consistency)

The empty sequent \vdash is not provable. Subsequently, it is impossible to prove both a formula A and its negation A\orth; it is impossible to prove \zero or \bot.

Proof. If a sequent is provable, then it is the conclusion of a cut-free proof. In each rule except the cut rule, there is at least one formula in conclusion. Therefore \vdash cannot be the conclusion of a proof. The other properties are immediate consequences: if \vdash A\orth and \vdash A are provable, then by the left negation rule A\orth\vdash is provable, and by the cut rule one gets empty conclusion, which is not possible. As particular cases, since \one and \top are provable, \bot and \zero are not, since they are equivalent to \one\orth and \top\orth respectively.

[edit] Expansion of identities

Let us write \pi:\Gamma\vdash\Delta to signify that π is a proof with conclusion \Gamma\vdash\Delta.

Proposition (η-expansion)

For every proof π, there is a proof π' with the same conclusion as π in which the axiom rule is only used with atomic formulas. If π is cut-free, then there is a cut-free π'.

Proof. It suffices to prove that for every formula A, the sequent A\vdash A has a cut-free proof in which the axiom rule is used only for atomic formulas. We prove this by induction on A.

  • If A is atomic, then A\vdash A is an instance of the atomic axiom rule.
  • If A=A_1\tens A_2 then we have
    
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \tens_R }
\BinRule{ A_1, A_2 \vdash A_1 \tens A_2 }
\LabelRule{ \tens_L }
\UnaRule{ A_1 \tens A_2 \vdash A_1 \tens A_2 }
\DisplayProof
    where π1 and π2 exist by induction hypothesis.
  • If A=A_1\parr A_2 then we have
    
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \parr_L }
\BinRule{ A_1 \parr A_2 \vdash A_1, A_2 }
\LabelRule{ \parr_R }
\UnaRule{ A_1 \parr A_2 \vdash A_1 \parr A_2 }
\DisplayProof
    where π1 and π2 exist by induction hypothesis.
  • All other connectives follow the same pattern.

The interesting thing with η-expansion is that, we can always assume that each connective is explicitly introduced by its associated rule (except in the case where there is an occurrence of the \top rule).

[edit] Reversibility

Definition (reversibility)

A connective c is called reversible if

  • for every proof \pi:\Gamma\vdash\Delta,c(A_1,\ldots,A_n), there is a proof π' with the same conclusion in which c(A_1,\ldots,A_n) is introduced by the last rule,
  • if π is cut-free then there is a cut-free π'.

Proposition

The connectives \parr, \bot, \with, \top and \forall are reversible.

Proof. Using the η-expansion property, we assume that the axiom rule is only applied to atomic formulas. Then each top-level connective is introduced either by its associated (left or right) rule or in an instance of the \zero_L or \top_R rule.

For \parr, consider a proof \pi\Gamma\vdash\Delta,A\parr
B. If A\parr B is introduced by a \parr_R rule (not necessarily the last rule in π), then if we remove this rule we get a proof of \vdash\Gamma,A,B (this can be proved by a straightforward induction on π). If it is introduced in the context of a \zero_L or \top_R rule, then this rule can be changed so that A\parr B is replaced by A,B. In either case, we can apply a final \parr rule to get the expected proof.

For \bot, the same technique applies: if it is introduced by a \bot_R rule, then remove this rule to get a proof of \vdash\Gamma, if it is introduced by a \zero_L or \top_R rule, remove the \bot from this rule, then apply the \bot rule at the end of the new proof.

For \with, consider a proof \pi:\Gamma\vdash\Delta,A\with B. If the connective is introduced by a \with rule then this rule is applied in a context like


\AxRule{ \pi_1 \Gamma' \vdash \Delta', A }
\AxRule{ \pi_2 \Gamma' \vdash \Delta', B }
\LabelRule{ \with }
\BinRule{ \Gamma' \vdash \Delta', A \with B }
\DisplayProof

Since the formula A\with B is not involved in other rules (except as context), if we replace this step by π1 in π we finally get a proof \pi'_1:\Gamma\vdash\Delta,A. If we replace this step by π2 we get a proof \pi'_2:\Gamma\vdash\Delta,B. Combining π1 and π2 with a final \with rule we finally get the expected proof. The case when the \with was introduced in a \top rule is solved as before.

For \top the result is trivial: just choose π' as an instance of the \top rule with the appropriate conclusion.

For \forall, consider a proof \pi:\Gamma\vdash\Delta,\forall\xi.A. Up to renaming, we can assume that ξ occurs free only above the rule that introduces the quantifier. If the quantifier is introduced by a \forall rule, then if we remove this rule, we can check that we get a proof of \Gamma\vdash\Delta,A on which we can finally apply the \forall rule. The case when the \forall was introduced in a \top rule is solved as before.

Note that, in each case, if the proof we start from is cut-free, our transformations do not introduce a cut rule. However, if the original proof has cuts, then the final proof may have more cuts, since in the case of \with we duplicated a part of the original proof.

A corresponding property for positive connectives is focalization, which states that clusters of positive formulas can be treated in one step, under certain circumstances.

[edit] One-sided sequent calculus

The sequent calculus presented above is very symmetric: for every left introduction rule, there is a right introduction rule for the dual connective that has the exact same structure. Moreover, because of the involutivity of negation, a sequent \Gamma,A\vdash\Delta is provable if and only if the sequent \Gamma\vdash A\orth,\Delta is provable. From these remarks, we can define an equivalent one-sided sequent calculus:

  • Formulas are considered up to De Morgan duality. Equivalently, one can consider that negation is not a connective but a syntactically defined operation on formulas. In this case, negated atoms \alpha\orth must be considered as another kind of atomic formulas.
  • Sequents have the form \vdash\Gamma.

The inference rules are essentially the same except that the left hand side of sequents is kept empty:

  • Identity group:
    
\LabelRule{\rulename{axiom}}
\NulRule{ \vdash A\orth, A }
\DisplayProof

\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Delta, A\orth }
\LabelRule{\rulename{cut}}
\BinRule{ \vdash \Gamma, \Delta }
\DisplayProof
  • Multiplicative group:
    
\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Delta, B }
\LabelRule{ \tens }
\BinRule{ \vdash \Gamma, \Delta, A \tens B }
\DisplayProof

\AxRule{ \vdash \Gamma, A, B }
\LabelRule{ \parr }
\UnaRule{ \vdash \Gamma, A \parr B }
\DisplayProof

\LabelRule{ \one }
\NulRule{ \vdash \one }
\DisplayProof

\AxRule{ \vdash \Gamma }
\LabelRule{ \bot }
\UnaRule{ \vdash \Gamma, \bot }
\DisplayProof
  • Additive group:
    
\AxRule{ \vdash \Gamma, A }
\LabelRule{ \plus_1 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof

\AxRule{ \vdash \Gamma, B }
\LabelRule{ \plus_2 }
\UnaRule{ \vdash \Gamma, A \plus B }
\DisplayProof

\AxRule{ \vdash \Gamma, A }
\AxRule{ \vdash \Gamma, B }
\LabelRule{ \with }
\BinRule{ \vdash, \Gamma, A \with B }
\DisplayProof

\LabelRule{ \top }
\NulRule{ \vdash \Gamma, \top }
\DisplayProof
  • Exponential group:
    
\AxRule{ \vdash \Gamma, A }
\LabelRule{ d }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof

\AxRule{ \vdash \Gamma }
\LabelRule{ w }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof

\AxRule{ \vdash \Gamma, \wn A, \wn A }
\LabelRule{ c }
\UnaRule{ \vdash \Gamma, \wn A }
\DisplayProof

\AxRule{ \vdash \wn\Gamma, B }
\LabelRule{ \oc }
\UnaRule{ \vdash \wn\Gamma, \oc B }
\DisplayProof
  • Quantifier group (in the \forall rule, ξ must not occur free in Γ):
    
\AxRule{ \vdash \Gamma, A[t/x] }
\LabelRule{ \exists^1 }
\UnaRule{ \vdash \Gamma, \exists x.A }
\DisplayProof

\AxRule{ \vdash \Gamma, A[B/X] }
\LabelRule{ \exists^2 }
\UnaRule{ \vdash \Gamma, \exists X.A }
\DisplayProof

\AxRule{ \vdash \Gamma, A }
\LabelRule{ \forall }
\UnaRule{ \vdash \Gamma, \forall \xi.A }
\DisplayProof

Theorem

A two-sided sequent \Gamma\vdash\Delta is provable if and only if the sequent \vdash\Gamma\orth,\Delta is provable in the one-sided system.

The one-sided system enjoys the same properties as the two-sided one, including cut elimination, the subformula property, etc. This formulation is often used when studying proofs because it is much lighter than the two-sided form while keeping the same expressiveness. In particular, proof-nets can be seen as a quotient of one-sided sequent calculus proofs under commutation of rules.

[edit] Variations

[edit] Exponential rules

  • The promotion rule, on the right-hand side for example,


\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B, \wn B_1, \ldots, \wn B_m }
\LabelRule{ \oc_R }
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
\DisplayProof
can be replaced by a multi-functorial promotion rule 
\AxRule{ A_1, \ldots, A_n \vdash B, B_1, \ldots, B_m }
\LabelRule{ \oc_R \rulename{mf}}
\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
\DisplayProof
and a digging rule 
\AxRule{ \Gamma \vdash \wn\wn A, \Delta }
\LabelRule{ \wn\wn}
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof
, without modifying the provability.

Note that digging violates the subformula property.

  • In presence of the digging rule 
\AxRule{ \Gamma \vdash \wn\wn A, \Delta }
\LabelRule{ \wn\wn}
\UnaRule{ \Gamma \vdash \wn A, \Delta }
\DisplayProof
, the multiplexing rule 
\AxRule{\Gamma\vdash A^{(n)},\Delta}
\LabelRule{\rulename{mplex}}
\UnaRule{\Gamma\vdash \wn A,\Delta}
\DisplayProof
(where A(n) stands for n occurrences of formula A) is equivalent (for provability) to the triple of rules: contraction, weakening, dereliction.

[edit] Non-symmetric sequents

The same remarks that lead to the definition of the one-sided calculus can lead the definition of other simplified systems:

  • A one-sided variant with sequents of the form \Gamma\vdash could be defined.
  • When considering formulas up to De Morgan duality, an equivalent system is obtained by considering only the left and right rules for positive connectives (or the ones for negative connectives only, obviously).
  • Intuitionistic linear logic is the two-sided system where the right-hand side is constrained to always contain exactly one formula (with a few associated restrictions).
  • Similar restrictions are used in various semantics and proof search formalisms.

[edit] Mix rules

It is quite common to consider mix rules: 
\LabelRule{\rulename{Mix}_0}
\NulRule{\vdash}
\DisplayProof
\qquad
\AxRule{\Gamma \vdash \Delta}
\AxRule{\Gamma' \vdash \Delta'}
\LabelRule{\rulename{Mix}_2}
\BinRule{\Gamma,\Gamma' \vdash \Delta,\Delta'}
\DisplayProof

Personal tools