Project topics and materials
Get Complete Project Material File(s) Now! »
Focusing Gentzen’s sequent calculus for classical logic: a survey
Classical sequent calculus LK was first introduced by Gentzen in 1934. The main purpose of this chapter is to investigate how classical sequent calculus can be modified and constructed with the features of focus and polarity. We therefore make a survey from Gentzen’s classical sequent calculus LK to the focused sequent calculus LKF which is introduced by Liang and Miller [LM09]. To make a focused sequent calculus for classical logic, linear logic plays an important role. Therefore we also present linear logic and linear sequent calculus[Gir87].
This chapter is presented with the following sections: Section 2.1 presents Gentzen’s LK system and one of its variants G3c . In Section 2.2 we introduce linear logic and its sequent calculus LL; then we present Girard’s system LC for classical logic, where the concept of polarity is first introduced. Section 2.3 presents the focused sequent calculus LLF for linear logic. Section 2.4 presents system LKF, a version of LLF for classical logic. For each system we discuss cut-elimination and its properties.
Gentzen’s sequent calculus
Gentzen [Gen35] introduced the sequent calculus as a formalism of mathematical logic and reason-ing, and sequent calculus is now a class of deduction systems. Perhaps the most well-known one is for classical first-order logic, but the notation and general principles are useful for many different logics and type theories, etc. We have already mentioned that proofs are labelled finite trees with a single root, with axioms at the top nodes, and each node-label connected with the labels of the successor nodes (if any) according to one of the rules. In (a bi-sided) sequent calculus, rules are divided into left-(L) and right-(R) rules. For any logical operator ∗, L∗ (resp. R∗) indicates the rules where a formula with ∗ as main operator as introduced on the left (resp. right). Gentzen’s original system for classical logic is called the LK system which is presented in Figure 2.1.
In this figure, a denotes an atomic formula and the notation {t }A represents the (capture-x avoiding) substitution of a (first-order) term t for x in the (first-order) formula A. Moreover, the left-hand side and the right-hand side of a sequent are here lists of formulae (hence the presence of the exchange rules (LExc) and (RExc)).
The connectives defined with the above rules are provably equivalent to those defined by the rules of Fig. 2.1, and the proofs of those equivalences critically rely on the structural rules.
Variants of Gentzen’s sequent calculus (system LK) for classical logic are presented in [TS00]. We will present here a popular variant: G3c , where structural rules are absorbed into the logical rules.
G3c system
We now look at the G3c system.
DEFINITION 1 (G3c system) Sequents of G3c system are of the form Γ ⊢ ∆. Here, Γ and are finite multisets of formulae, and are called the context: more precisely, Γ is called the antecedent and ∆ is called the succedent of a sequent. The formula that appears explicitly in the conclusion of each rule is called the principal formula or main formula. The formulae in the premises from which the principal formula is derived are the active formulae. The other formulae are called side formulae. The G3c system is defined in Figure 2.2, where a denotes an atomic formula.1
Cut-rules express a form of transitivity of ⊢, and can be seen as general forms of a lemma: it says that when a formula A is in the succedent of a proved sequent and in the antecedent of another proved sequent, then by “cutting out” the formula A (which is called the cut-formula) we build a proof of the remaining context; in other words, to prove Γ ⊢ ∆, we first prove A as a lemma, and then continue the proof with A as an extra assumption.
In rule Ax, both occurrences of a are principal; in L⊥ the occurrence of ⊥ is principal.
But an important property of the rules of Fig. 2.2 is the sub-formula property: every formula in the premises of a rule is the sub-formula of some formula in the conclusion of the rule. This is not the case of cuts, as it is not necessary that the cut-formula A in the premises is a sub-formula of a formula in Γ, ∆. This is problematic for bottom-up proof-search, as the formula A has to be guessed (and there are infinitely many possibilities).
Cut-elimination
However, a major theorem of sequent calculus is the Hauptsatz [Gen35] or cut-elimination theorem. This theorem says that cuts are admissible; i.e. every formula that is provable using cuts, is also provable without cuts.
In [TS00], the cut-elimination proof is based on certain local transformation steps, defining an algorithm that permutes for instance cut-rules upwards, over the other rules, or replaces a cut on a compound formula A by some cuts on its immediate sub-formulae.
However, by either forbidding a cut to permute over another cut, or by carefully controlling when that happens, it is possible to make the cut-elimination procedure strongly normalising.
Another question is confluence: The design of a cut-elimination process by local rewrite steps raises the question of whether, when permuting a cut upwards, we should start pushing it into its left-hand-side branch first or into its right-hand-side branch first. The following example is due to Lafont:
Consider two distinct (cut-free) proofs, π1 and π2 , of the sequent Γ ⊢ ∆. Since weakenings are admissible, we can easily get two proofs π1′ and π2′ of Γ ⊢ ∆, A and Γ, A ⊢ ∆, respectively. In essence, these are the same as π1 and π2 , but with an extra formula that is added to every sequent of the proof-tree, not participating to any of the inference rules. Cutting them gives a new proof of Γ ⊢ ∆:
Eliminating that cut can be done in two ways: pushing the cut to the left eventually yields π1 , erasing π2 , while pushing the cut to the right eventually yields π2 , erasing π1 .
This shows that, in general, this kind of cut-elimination in classical logic is not confluent, as the complete duality illustrated by De Morgan’s laws leads to a symmetry that gives us no particular reason to give priority to the left or to the right.
A similar example (actually more problematic than the one above) can be build with con-tractions: Consider two distinct (cut-free) proofs, π1 and π2 , of the sequents Γ ⊢ ∆, A, A and Γ, A, A ⊢ ∆, respectively. Since contractions are admissible, we can easily get two proofs π1′ and π2′ of Γ ⊢ ∆, A and Γ, A ⊢ ∆, respectively. Cutting them gives a proof of Γ ⊢ ∆:
Linear logic and the sequent calculus LC for classical logic
In this section, we discuss linear logic and a sequent calculus for it [Gir87]; then we present a polarised sequent calculus LC for classical logic, inspired by linear logic.
Linear logic and its sequent calculus
Linear logic is a refinement of e.g. classical and intuitionistic logic, with new connectives that can be used to decompose the usual connectives. This logic plays an important role in modern computer science and engineering. Now, we give a brief idea of linear logic and then we present a sequent calculus LL.
An important feature of linear logic is a duality between connectives and formulae, similar to the De Morgan duality of classical logic. As in classical logic, a great role is played by the involutive negation function, here called linear negation and denoted (•)⊥ ; we use it to internalise De Morgan laws for all connectives and quantifiers. For instance, ∃xA is the dual of ∀xA⊥ and = A⊥⊥.
The main feature of linear logic is the controlled use of the structural rules of weakening and contraction. Girard criticised these structural rules from Gentzen’s sequent calculus in [Gir95], because weakening generates “fake dependencies”, for instance when proving A ⇒ (B ∨ ¬B). Hence the introduction of a linear implication ⊸, where the premise must be “used” exactly once. Restricting the structural rules of weakening and contraction leads to breaking the property described in Remark 1: the choice of inference rules for the conjunction and disjunction becomes critical, and the two versions then lead to two different connectives that are not equivalent. Therefore, linear logic presents two disjunctions: ⊕ (plus) and ` (par). Intuitively, a ⊕ disjunction is proved by proving one (and only one) of its two sides (as in intuitionistic logic), whereas a ` disjunction can be proved by “keeping” both sub-formulae and possibly relate them, just like A ¬A can be proved in classical logic. Moreover, similarly to classical logic, an implication A ⊸ B can be seen as an abbreviation for (A)⊥ ` B.
Dually, there are also two conjunctions in linear logic: ⊗ (times) and & (with). The former is the dual of ` and the latter is the dual of ⊕.
This duality plays an important role in the proof of cut-elimination, which also hold in linear logic (see next section) and whose details give an intuition about the connectives: Both conjunc-tions express the “availability of two possibilities”, but in the case of &, only one of the possibilities will be used during cut-elimination (as it will face a ⊕ disjunction), and in the case of ⊗, both possibilities will be used.
Linear quantifier ∀ is close to & and ∃ is close to ⊕.
Now, weakening and contractions are not completely ruled out of the system, they are controlled by two new connectives: ! and ?, that are called exponentials.
Girard also presents a sequent calculus LL for linear logic [Gir87]. The preliminaries for LL and the system are given below:
DEFINITION 2 (Formulae, negation)
The notion of atoms from Gentzen’s sequent calculus is here enriched as the notion of literals: atoms equipped with an involutive negation function mapping a literal a to a literal a⊥ . Formulae of LL are given by the following grammar:
A, B, := a | 1 | ⊥ | ⊤ | 0 | A ⊗ B | A ` B | A&B | A ⊕ B | ∀xA | ∃xA |!A |?A where a ranges over literals.
DEFINITION 3 (LL system)
We use the De Morgan duality to avoid the redundancy of having both the left-introduction rule(s) for a connective and the right-introduction rule(s) for the dual connective:2
The sequent calculus LL is mono-sided, with sequents of the form ⊢ ∆ where ∆ is a multiset of formulae. Its rules are given in Figure 2.3. ※
Linear connectives are presented in three categories:
Multiplicative connectives: The connectives ⊗, `, ⊸, together with the neutral elements 1 (w.r.t. ⊗) and ⊥ (w.r.t. `) are called multiplicative connectives.
Additives connectives: The connectives & and ⊕, together with the neutral elements ⊤ (w.r.t &) and 0 (w.r.t ⊕) are called additive connectives.
Exponential connectives: The connectives ! and ? are called exponential connectives, and are also called linear modalities.
It is interesting to note that:
⊗ is multiplicative and conjunctive with neutral 1,
⊕ is additive and disjunctive with neutral 0,
` is disjunctive with neutral ⊥ and
Cut-elimination
Once again, designing a cut-elimination process by local rewrite steps raises the question of whether, when permuting a cut upwards, we should start pushing it into its left-hand-side branch first or into its right-hand-side branch.
And in linear logic as in classical logic, the complete duality illustrated by De Morgan’s laws leads to a symmetry that gives us no particular reason to give priority to the left or to the right.
However, the two examples of non-confluence in the previous section are prevented in linear logic by its tight control on the structural rules: weakenings and contractions can only be done on formulae of the form ?A, which will only be cut against the formula !A⊥ that cannot be weakened or contracted; hence, there cannot be a weakening on both sides of the cut, nor a contraction.
Table of contents :
1 Introduction
2 Focusing Gentzen’s sequent calculus for classical logic: a survey
2.1 Gentzen’s sequent calculus
2.2 Linear logic and the sequent calculus LC for classical logic
2.2.1 Linear logic and its sequent calculus
2.2.2 The sequent calculus LC
2.3 Introducing focusing in linear logic
2.3.1 Preliminaries
2.3.2 The triadic system LLF
2.4 The focused sequent calculus LKF for classical logic
3 A sequent calculus for classical logic modulo theories
3.1 LKp(T ): Definitions
3.2 Admissibility of basic rules
3.3 Invertibility of the asynchronous phase
3.4 On-the-fly polarisation
3.5 Cut-elimination
3.5.1 Cuts with the theory
3.5.2 Safety and instantiation
3.5.3 More general cuts
3.6 Changing the polarity of connectives
3.7 Completeness
4 Simulating SMT-solving in the sequent calculus
4.1 Variations on Davis-Putnam-Logemann-Loveland
4.1.1 DPLL
4.1.2 DPLL-modulo-theories
4.1.3 The Elementary DPLL(T ) system
4.2 Preliminaries
4.3 An indirect simulation of DPLL(T )
4.3.1 The LKDPLL(T ) system
4.3.2 Simulation of DPLL(T ) in LKDPLL(T )
4.3.3 Simulation of LKDPLL(T ) in LKp(T )
4.4 Direct simulation of DPLL(T )
4.4.1 Simulating Elementary DPLL(T )
4.4.2 Turning the simulation into a bisimulation
4.4.3 Extending the simulation with backjump and lemma learning
5 Simulating clause and connection tableaux in the sequent calculus
5.1 Clause and connection tableaux
5.2 Simulation of clause tableaux (modulo theories)
5.3 Simulation of weak connection tableaux
5.4 Simulation of strong connection tableaux
5.5 Extending the simulations to pure first-order logic
5.5.1 Preliminaries
5.5.2 Clause and connection tableaux in first-order logic
5.5.3 The LKpd
F system and the simulation of clause tableaux
5.5.4 The LKpdp
F system and the simulation of weak connection tableaux
6 Conclusion
Bibliography
Index
List of figures
