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.
Atomic formulas, written α,β,γ, are predicates of the form , 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:
|of course||why not||exponentials|
|there exists||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 and why not A for . 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 in classical logic, as .
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 is a formula with variables xi, then the formula A[B / X] is A where every atom is replaced by .
Sequents and proofs
A sequent is an expression where Γ and Δ are finite multisets of formulas. For a multiset , the notation represents the multiset . Proofs are labelled trees of sequents, built using the following inference rules:
- Identity group:
- Multiplicative group:
- Additive group:
- Exponential group:
- of course:
- why not:
- Quantifier group (in the and rules, ξ must not occur free in Γ or Δ):
- there exists:
- for all:
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 modality. This is what distinguishes linear logic from classical logic: if weakening and contraction were allowed for arbitrary formulas, then and would be identified, as well as and , and , and . By identified, we mean here that replacing a with a 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:
Two formulas A and B are (linearly) equivalent, written , if both implications and are provable. Equivalently, if both and are provable. Another formulation of is that, for all Γ and Δ, is provable if and only if is provable.
De Morgan laws
Negation is involutive:
Duality between connectives:
- Associativity, commutativity, neutrality:
- Idempotence of additives:
- Distributivity of multiplicatives over additives:
- Defining property of exponentials:
- Monoidal structure of exponentials:
- Other properties of exponentials:
These properties of exponentials lead to the lattice of exponential modalities.
- Commutation of quantifiers (ζ does not occur in A):
The units and the additive connectives can be defined using second-order quantification and exponentials, indeed the following equivalences hold:
The constants and and the connective can be defined by duality.
Any pair of connectives that has the same rules as is equivalent to it, the same holds for additives, but not for exponentials.
Other basic equivalences exist.
Properties of proofs
Cut elimination and consequences
Theorem (cut elimination)
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:
Theorem (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.
Expansion of identities
Let us write to signify that π is a proof with conclusion .
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 rule).
A corresponding property for positive connectives is focalization, which states that clusters of positive formulas can be treated in one step, under certain circumstances.
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 is provable if and only if the sequent 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 must be considered as another kind of atomic formulas.
- Sequents have the form .
The inference rules are essentially the same except that the left hand side of sequents is kept empty:
- Identity group:
- Multiplicative group:
- Additive group:
- Exponential group:
- Quantifier group (in the rule, ξ must not occur free in Γ):
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.
- The promotion rule, on the right-hand side for example,
can be replaced by a multi-functorial promotion rule and a digging rule , without modifying the provability.
Note that digging violates the subformula property.
- In presence of the digging rule , the multiplexing rule (where A(n) stands for n occurrences of formula A) is equivalent (for provability) to the triple of rules: contraction, weakening, dereliction.
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 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.
It is quite common to consider mix rules: