THIS IS WORK IN PROGRESS
One of the greatest insights of Gentzen, in the devolpment of natural deduction, was to notice that the meaning of logical connectives and quantifiers can be understood not by an arbitrary set of axioms, but by how they are proved (or introduced) and how they are used to prove other propositions (or eliminated), in closer connection to mathematical reasoning practices. For instance, given propositions A and B, if I were to prove the conjuction A & B, I would go about proving proposition A and proposition B, separately. We can capture this idea in the following introduction rule:
Γ ⊢ A Γ ⊢ B
--------------&I
Γ ⊢ A & B
Γ being a (finite) set of hypotheses and Γ ⊢ A denoting the judgment "proposition A is true if we assume all propositions in Γ to be true". If I have A & B on the other hand, I might use it to extract a proof of A and/or a proof of B:
Γ ⊢ A & B Γ ⊢ A & B
---------&E1 ---------&E2
Γ ⊢ A Γ ⊢ B
To prove an implication A → B, however, I must show that A entails B; that is, that by assuming A, I can prove B. This is captured by the rule:
Γ, A ⊢ B
---------→I
Γ ⊢ A → B
And in order to use A → B to prove B, I must have a proof of A:
Γ ⊢ A → B Γ ⊢ A
-------------------→E
Γ ⊢ B
Now, to introduce a disjunction A ∨ B, I must either provide a proof of A or a proof of B.
Γ ⊢ A Γ ⊢ B
---------∨I1 ---------∨I2
Γ ⊢ A ∨ B Γ ⊢ A ∨ B
However, to use A ∨ B to prove a new proposition C, this proposition must be entailed by both A and B:
Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C
-----------------------------------∨E
Γ ⊢ C
The trivial proposition (top) has a simple introduction rule
------⊤I
Γ ⊢ ⊤
but no elimination rules. Finally, there are no introduction rules for the absurd proposition (bottom). It however, by the principle of explosion, entails everything:
Γ ⊢ ⊥
-----⊥E
Γ ⊢ C
A proof of a proposition built up by connectives and primitive propositions will therefore be a tree of such valid inference rules, where at the leaves of this tree will be the immediate identity rules:
-----id
Γ ⊢ A
when A ∈ Γ. That is, if A is among the assumptions, then A is true. For instance, a proof of A → (B → (A & B)) might go as follows (the proof should be read bottom-up):
--------id --------id
A, B ⊢ A A, B ⊢ B
---------------------&I
A, B ⊢ A & B
---------------→I
A ⊢ B → (A & B)
--------------------→I
⊢ A → (B → (A & B))
Now, in order to be sure that these rules are sound, we must show that the absurd proposition ⊥ is not provable in the absence of hypotheses.1 Looking at the rules, we see that no introduction rules can ever introduce ⊥; however, we never know a priori whether an elimination rule might be used to prove it. Consider the elimination rule for →:
⊢ A → ⊥ ⊢ A
----------------→E
⊢ ⊥
That is, in order to show that ⊢ ⊥ is impossible, we must also show that there exists no proposition A, which has no a priori connection to ⊥, such that both ⊢ A → ⊥ and ⊢ A hold. This only complicates the matter even more. Furthermore, Gentzen noticed that his natural deduction would allow for roundabout proofs which could be simplified. To illustrate this, suppose we have a proof trees 𝔇 and 𝔈 of A and B respectively. Then we can find a new roundabout, and redundant, proof of A:
𝔇 𝔈
⊢ A ⊢ B
----------&I
⊢ A & B
--------&E1
⊢ A
Notice how this new proof of A also depends on the proof of an entirely separate proposition B.2 Gentzen found this to be a flaw in his natural deduction. The culprit, as he discovered, were the elimination rules, which do not obey the subformula(subproposition) property. By this he means that some propositions which appear in the premises of such elimination rules, do not appear at all at their conclusions. It seems reasonable, afterall, that for a sound logic system, a non-roundabout, canonical, proof of Γ ⊢ A should only depend on what is in Γ and A, and that every other proof could be simplified, or normalized, to such a canonical proof. Indeed, if this is correct, then ⊢ ⊥ could never be proved.
Gentzen then set to find a new proof calculus which rules would all have the subformula property, and therefore would contain no roundabout proofs. Enter the sequent calculus.
Firstly, what Gentzen called sequents were the pairs (Γ, A) found in the judgments of form Γ ⊢ A; Γ being called the antecedent and A the succedent. Unlike Gentzen, we assumed the antecedent (the hypotheses) to be a set instead of a sequence, as the order in which the proposition appear do not yet matter.
Now, the sequent calculus is divided into two classes of rules: those that act on the succedent, called the right rules, and those that act on the antecedent, called the left rules. Fortunately, the right rules coincide with introduction rules of natural deduction. The left rules, however, are quite different, since they must obey the subformula property. Here are the rules:
Γ, A & B, A, B ⊢ C
------------------&L
Γ, A & B ⊢ C
Γ, A ∨ B, A ⊢ C Γ, A ∨ B, B ⊢ C
-----------------------------------∨L
Γ, A ∨ B ⊢ C
Γ, A → B, B ⊢ C Γ, A → B ⊢ A
--------------------------------→L
Γ, A → B ⊢ C
--------⊥L
Γ, ⊥ ⊢ C
These rules can be respectively summed up, intuitively, as follows:
- Assuming
A & B, you can also safely assume bothAandB. This one is quite obvious. - Assuming
A ∨ B, if you can proveCwith the help of each one ofAandBseparately, then you can already proveC. The idea here is that whichever caseA ∨ B(AorB) is, you have shown how to proveCfrom either case. - Assuming
A → B, if you can proveAand, with the help ofB, you are able to proveC, then you are able to proveC. This is the case because if you can proveA, then, because of the implicationA → B, you would also be able to proveB; thus,Cwould also be provable. - Assuming
⊥, anything is provable. This is the principle of explosion.
A sample proof in the sequent calculus would go like this (again, it should be read bottom-up)
-------------id -------------id -------------id -------------id
..., A, B ⊢ A ..., A, B ⊢ B ..., A, C ⊢ A ..., A, C ⊢ C
------------------------------&R -------------------------------&R
..., A, B ⊢ A & B ..., A, C ⊢ A & C
-----------------------------∨R1 ------------------------------∨R2
..., A, B ⊢ (A & B) ∨ (A & C) ..., A, C ⊢ (A & B) ∨ (A & C)
---------------------------------------------------------------------∨L
..., A, B ∨ C ⊢ (A & B) ∨ (A & C)
---------------------------------&L
A & (B ∨ C) ⊢ (A & B) ∨ (A & C)
-------------------------------------→R
⊢ (A & (B ∨ C)) → ((A & B) ∨ (A & C))
The ellipses ... denote the other sets of assumptions which are not relevant in the proof.
Now, although these rules look almost completely different from the elimination rules, they are already contained in natural deduction, as derived rules. Here are the respective left rules, proven in natural deduction:
Γ, A & B, A, B ⊢ C
-------------------→I ----------------id
Γ, A & B, A ⊢ B → C Γ, A & B ⊢ A & B
----------------------→I ----------------&E1 ----------------id
Γ, A & B ⊢ A → (B → C) Γ, A & B ⊢ A Γ, A & B ⊢ A & B
--------------------------------------→E ----------------&E2
Γ, A & B ⊢ B → C Γ, A & B ⊢ B
---------------------------------------------------------------→E
Γ, A & B ⊢ C
----------------id
Γ, A ∨ B ⊢ A ∨ B Γ, A ∨ B, A ⊢ C Γ, A ∨ B, B ⊢ C
--------------------------------------------------------∨E
Γ, A ∨ B ⊢ C
----------------id
Γ, A → B, B ⊢ C Γ, A → B ⊢ A → B Γ, A → B ⊢ A
----------------→I ---------------------------------→E
Γ, A → B ⊢ B → C Γ, A → B ⊢ B
--------------------------------------→E
Γ, A → B ⊢ C
--------id
Γ, ⊥ ⊢ ⊥
--------⊥E
Γ, ⊥ ⊢ C
This means that natural deduction is just as strong as, or stronger, than the sequent calculus. There is one rule however, that we can add
1 Since by using ⊥ elimination rule, we can prove any proposition. Our proof system would thus be useless.
2 This fact makes it really hard to have a proof search algorithm for natural deduction, as such an algorithm would have to guess and synthetize entirely new propositions for such cases.