Understanding properties and criticisms of a (specific) sequent calculus

Question

In Ebbinghaus et al., Mathematical Logic, a sequent calculus with the following rules is used:

(Ant) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma' & \varphi\end{array}$, if $\Gamma \subseteq \Gamma'$ $\qquad$ (Assm) $\begin{array}{ll} \\ \hline \Gamma & \varphi\end{array}$, if $\varphi \in \Gamma$

(PC) $\begin{array}{lll} \Gamma & \psi & \varphi \\ \Gamma & \lnot \psi & \varphi \\ \hline \Gamma & & \varphi\end{array}$ $\qquad\qquad$ (Ctr) $\begin{array}{lll} \Gamma & \lnot\varphi & \psi \\ \Gamma & \lnot \varphi & \lnot \psi \\ \hline \Gamma & & \varphi\end{array}$

($\lor A$) $\begin{array}{lll} \Gamma & \varphi & \chi \\ \Gamma & \psi & \chi\\ \hline \Gamma & (\varphi\lor\psi) & \chi\end{array}$ $\qquad$ ($\lor S$) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\varphi\lor\psi)\end{array}$, $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\psi\lor\varphi)\end{array}$

($\exists A$) $\begin{array}{lll} \Gamma & \varphi\frac{y}{x} & \psi \\ \hline \Gamma & \exists x\varphi & \psi\end{array}$, if $y$ is not free in $\Gamma \; \exists x\varphi \; \psi$

($\exists S$) $\begin{array}{ll} \Gamma & \varphi\frac{t}{x} \\ \hline \Gamma & \exists x\varphi\end{array}$

($\equiv$) $\begin{array}{l} \\ \hline t \equiv t\end{array}$ $\qquad\qquad$ (Sub) $\begin{array}{lll} \Gamma & & \varphi\frac{t}{x} \\ \hline \Gamma & t \equiv t' & \varphi\frac{t'}{x}\end{array}$

It looks like this calculus only consists of deduction rules, without any axiom schemes. Is this correct? Or should we interpret (Assm) and ($\equiv$) as axiom schemes, because they deduce something from nothing? What about (Ant) and (Sub), where the conclusion isn't uniquely determined by the premisses, because it can contain arbitrary formulas or terms?

[Bonus question: The Hilbert system only has two deduction rules, but many axioms and axiom schemes. With the Hilbert system, I often had to look up "formal proofs" somewhere, because I didn't manage to find them myself. With the sequent calculus, I seem to be able to find the formal proofs myself. Is there a mathematical explanation for this phenomenon?]

In his review of the cited book, Peter Smith sharply criticizes the chosen deduction system:

Ch. 4 is called ‘A Sequent Calculus’. The version chosen is really, really, not very nice. For a start (albeit a minor point that only affects readability), instead of writing a sequent as $\text{‘}\Gamma \vdash \varphi\text{’}$, or $\text{‘}\Gamma \Rightarrow \varphi\text{’}$, or even $\text{‘}\Gamma : \varphi\text{’}$, EFT just write an unpunctuated $\text{‘}\Gamma \; \varphi\text{’}$. Much more seriously, they adopt a system of rules which many would say mixes up structural rules and classical logical rules for the connectives in an unprincipled way (thereby losing just the insights that a sequent system can be used to highlight). [To be more specific, they introduce a classical ‘Proof by Cases’ rule that takes us from the sequents (in their notation) $\Gamma \; \psi \; \varphi$ and $\Gamma \; \lnot \psi \; \varphi$ to $\Gamma \; \varphi$, and then appeal to Proof by Cases to get Cut as a derived rule. This really muddies the waters in various ways!]

The closest thing to (Cut) that is derived as a consequence of the rules in the book the Chain Rule:

(Ch) $\begin{array}{lll} \Gamma & & \varphi \\ \Gamma & \varphi & \psi \\ \hline \Gamma & & \psi \end{array}$ $\quad$ while (Cut) would be $\begin{array}{lcr} \Gamma & \vdash & \Delta \; \varphi \\ \varphi \; \Lambda & \vdash & \psi \\ \hline \Gamma \; \Lambda & \vdash & \Delta \; \psi \end{array}$ or $\begin{array}{lll} \Gamma & & \varphi \\ \varphi & \Lambda & \psi \\ \hline \Gamma & \Lambda & \psi \end{array}$

I don't see how (Ch) or (Cut) could replace (PC). I'm not sure whether this is related to the fact that the above calculus interprets a sequent $\phi \; \varphi \; \psi \; \chi$ as $\phi \rightarrow (\varphi \rightarrow (\psi \rightarrow \chi))$, so that each sequent must have exactly one succedent, and the $\vdash$ sign can be omitted. Is it possible to add (Cut) as rule, remove one of the other rules and possibly adjust the remaining rules slightly, and get the same calculus (where the unmodified original rules can be obtained as derived rules)?

Answer 1

Yes, (Assm) and ($\equiv$) are axioms -- formally an axiom is neither more or less than a rule of inference that requires no premises.

It's not a particular problem that a named rule of inference has instances that concludes different things from identical premises -- except notationally: of course it means that you cannot reconstruct a proof sequence from knowing which axioms are used where and which named rules used with which premises in each line. But that is not a peculiarity of this particular calculus; "structural rules" such as (Ant) are standard fare in many proof systems.

---

The (Ch) rule is morally equivalent to your formulation of (Cut). If you have $\Gamma\varphi$ and $\varphi\Lambda\psi$, then you can conclude $\Gamma\Lambda\varphi$ and $\Gamma\Lambda\varphi\psi$ from them by applying Ant to each of them. Then (Ch) concludes $\Gamma\Lambda\psi$.

It doesn't look like the quote from Peter Smith claims that Cut could replace the (PC) rule. Even in proper sequent calculus, Cut doesn't replace anything -- thanks to the cut elimination theorem it isn't even necessary there.

However, in Ebbinghaus' system, both of (PC) and (Ctr) are "cut-like" in that their premises contains a formula $\psi$ that disappears completely in the conclusion. Usually in sequent calculi, Cut is the only rule where a premise can contain a formula that has a more complex structure than any formula in the conclusion. And, as noted above, Cut isn't even necessary there.

Here, on the other hand, (PC) and (Ctr) are necessary -- if we remove them, we completely lose the ability to reason about negation, and with it the ability to reason about implication (which I suppose is to be treated as an abbreviation for $\neg p\lor q$).

And it is really most un-sequentlike to lack ($\neg$A) and ($\neg$S) rules. Instead, the (Ctr) rule is perverse enough to add more connectives to formula from the conclusion when building its premises.

---

Later edit: Here is a set of natural sequent-like ($\neg$A) and ($\neg$S) rules in the syntax of Ebbinghaus:

$$(\neg A) \frac{\Gamma\quad \varphi}{\Gamma\quad\neg\varphi\quad\psi} \qquad (\neg S) \frac{\Gamma\quad \varphi\quad \mathcal A}{\Gamma\quad\neg\varphi} \text{ where }\mathcal A\text{ is a propositional variable not free in }\Gamma, \varphi $$

However, these rules are not enough to make $\neg p\lor q$ work well as a representation of $p\to q$ -- the usual elimination rule for $\to$ goes through fine, but $\to$ cannot be introduced sensefully if it's built on a disjunction that works intuitionistically. Adding one of (PC) or (Ctr) back in would probably save that, however.

Answer 2

I think that, in spite of the "advice" that :

the above calculus interprets a sequent $\phi \; \varphi \; \psi \; \chi$ as $\phi \rightarrow (\varphi \rightarrow (\psi \rightarrow \chi))$, so that each sequent must have exactly one succedent, and the $\vdash$ sign can be omitted

there is a more "natural" way to read the above rules.

Consider the definition od sequent [page 59] :

If we call a nonempty list (sequence) of formulas a sequent, then we can use sequents to describe stages in a proof. For instance, the stage with assumptions $\varphi_0, ... \varphi_{n-1}$ and claim $\varphi$ is rendered by the sequent $\varphi_0, ... \varphi_{n-1} \varphi$.

Thus, we can easily "restore" the $\vdash$ sign in order to go back to a more "natural" set of rules.

Of course, (Ant) is a Weakening rule and (Assm) is the Assumption rule.

About the more "complicated" rules, the "intended reading" is :

($\lor A$) $\begin{array}{lll} \Gamma , \varphi \vdash \chi \\ \Gamma , \psi \vdash \chi\\ \hline \Gamma , (\varphi\lor\psi) \vdash \chi\end{array}$ $\qquad$ ($\lor S$) $\begin{array}{ll} \Gamma \vdash \varphi \\ \hline \Gamma \vdash (\varphi\lor\psi)\end{array}$, $\begin{array}{ll} \Gamma \vdash \varphi \\ \hline \Gamma \vdash (\psi\lor\varphi)\end{array}$

($\exists A$) $\begin{array}{lll} \Gamma , \varphi\frac{y}{x} \vdash \psi \\ \hline \Gamma , \exists x\varphi \vdash \psi\end{array}$, if $y$ is not free in $\Gamma , \; \exists x\varphi \; \psi$

($\exists S$) $\begin{array}{ll} \Gamma \vdash \varphi\frac{t}{x} \\ \hline \Gamma \vdash \exists x\varphi\end{array}$

and so on ...

In this way, also the Chain Rule seems less horrible :

(Ch) $\begin{array}{lll} \Gamma \vdash \varphi \\ \Gamma , \varphi \vdash \psi \\ \hline \Gamma \vdash \psi \end{array}$ $\quad$

and it is "quite similar" to the usual (Cut).

As remarked by Henning, the $\rightarrow$ connective is defined through $\lnot p \lor q$ [see page 34], and thus modus ponens is a derived rule [page 63], using (Ch) :

$\begin{array}{lll} \Gamma \vdash \lnot \varphi \lor \psi \\ \Gamma \vdash \varphi \\ \hline \Gamma \vdash \psi \end{array}$

Of course, in this way the classical "semantics" is "embedded" into the system.

Finally, the choice of the name for the $\lnot$-rules is quite objectionable; while the Contradiction Rule (Ctr) is clearly (RAA), in presence of ($\lor$A), which is a proof by cases rule, the Proof by Cases Rule (PC) would be better to call it (following Tennant) Dilemma.

In conclusion, all these innovations was worth it ?

Answer 3

I think now that the "inspiration" for Ebbinghaus et al.'s deductive calculus is Tait calculus [1].

See

• Helmut Schwichtenberg, Proof Theory : Some Applications of Cut-Elimination, in Jon Barwise (editor), Handbook of mathematical logic (1999), page 867-on

and

• Helmut Schwichtenberg & Stanley Wainer, Proofs and Computations (2012), page 57 :

[This calculus "embed" classical logic through] the de Morgan laws ($¬(A∧B)↔ ¬A∨¬B,¬∀xA ↔ ∃x¬A$, etc.) and these allow any formula to be brought into negation normal form, i.e., built up from atoms or negated atoms by applying $∨, ∧, ∃, ∀$. For such formulas Tait [1968] derived a deceptively simple calculus with just one rule for each symbol.

The rules of Tait’s calculus are as follows where, in order to single out a particular formula from a finite set, the convention is that $\Gamma, A$ denotes the finite set $\Gamma \cup \{ A \}$.

$$\Gamma, Rx, \lnot Rx \, \, \text{(Ax)}$$

$${\Gamma , A_0, A_1 \over \Gamma, (A_0 \lor A_1)}\, \, (\lor)$$

$${\Gamma , A_0 \quad \Gamma, A_1 \over \Gamma, (A_0 \land A_1)}\, \, (\land)$$

$${\Gamma , A(t) \over \Gamma, \exists xA(x)}\, \, (\exists)$$

$${\Gamma , A \over \Gamma, \forall xA}\, \, (\forall)$$

$${\Gamma , C \quad \Gamma, \lnot C \over \Gamma}\, \, \text{(Cut)}$$

where in the axioms $Rx$ is an atom, and in the $∀$-rule $x$ is not free in $\Gamma$.

That this is an equivalent formulation of classical logic is easy. First notice that any finite set derivable as above is, when considered as a disjunction, valid in all classical models and therefore (by completeness) classically derivable. In the opposite direction, if $\Gamma \vdash_C A$ [i.e. derivable in classical natural deduction], then $¬\Gamma, A$ is derivable in the pure Tait calculus.

---

Footnote :

[1] Originally published as W.W. Tait, NORMAL DERIVABILITY IN CLASSICAL LOGIC, in Jon Barwise (editor), The Syntax and Semantics of Infinitary Languages (1968), page 204-on.