Sequent and Gentzen calculus formulae

Question

The text I am following at present, V. Manca's Logica matematica ('mathematical logic' in Italian), introduces sequent calculus by explaining how the tableau rules generating children in the tree can be classed in $\alpha$, $\beta$, $\gamma$ and $\delta$ rules: $$\alpha=(T:\varphi\land\psi)\Rightarrow\alpha_1=(T:\varphi),\alpha_2=(T:\psi);\quad\alpha=(F:\varphi\lor\psi)\Rightarrow\alpha_1=(F:\varphi),\alpha_2=(F:\psi)$$

$$\beta=(T:\varphi\lor\psi)\Rightarrow\beta_1=(T:\varphi),\beta_2=(T:\psi);\quad\beta=(F:\varphi\land\psi)\Rightarrow\beta_1=(F:\varphi),\beta_2=(F:\psi)$$$$\gamma=(T:\forall x\varphi(x))\Rightarrow\gamma(t)=(T:\varphi(t));\quad\gamma=(F:\exists x\varphi(x))\Rightarrow\gamma(t)=(F:\varphi(t))$$$$\delta=(T:\exists x\varphi(x))\Rightarrow\delta(a)=(T:\varphi(a));\quad\delta=(F:\forall x\varphi(x))\Rightarrow\delta(a)=(F:\varphi(a))$$where $T$ means true and $F$ false. If I correctly understand, $(T:\chi)$ is equivalent to $\chi$, $(F:\chi)$ is equivalent to $\lnot\chi$, and, very roughly speaking, the $\alpha$ rules are those generating childen belonging to the same branch of the parent formula, the $\beta$ rules are "disjunctive", generating childen belonging to two different branches of the parent formula, the $\gamma$ rules substitute a variable $t$ that can represent any element and the $\delta$ rules substitute a constant $a$ that represent the existing element satisfying respectively the truth (first case) or the falsity (second case) of $\varphi(a)$.

In such a way -the book says- the tableau rules can be expressed in the following way, where $S$ indicates a set of marked formulae and where the label letters are upside down with respect with the usual tree form:$$\frac{S,\alpha_1,\alpha_2}{S,\alpha}\quad\frac{S,\beta_1|S,\beta_2}{S,\beta}\quad\frac{S,\gamma,\gamma(t)}{S,\gamma}\quad\frac{S,\delta(a)}{S,\delta} $$(where I would say that $|$ corresponds to the bifurcation of the tree, to a disjunction, and the commas represent conjunctions, the presence of the formulae, between which they are placed, on the same branch of the tableau tree) and, the text says, *if we use the notation $[]$ for sequents, we get the following compact notation*$$\frac{[S,\alpha_1,\alpha_2]}{[S,\alpha]}\quad\frac{[S,\beta_1]\quad[S,\beta_2]}{[S,\beta]}\quad\frac{[S,\gamma(t)]}{[S,\gamma]}\quad\frac{[S,\delta(a)]}{[S,\delta]} .$$ Here my problems of understanding begin, indeed I know that a sequent is a formula $\Phi\vdash\Psi$ meaning that from all the formulae in $\Phi$ at least one of the formulae in $\Psi$ follows, but I am not sure how that appears in those formulae. Then the text says that, if we rewrite these rules in the original sequent notation we get $$\frac{\Gamma,\varphi,\psi\vdash\Delta}{\Gamma,\varphi\land\psi\vdash\Delta}\quad\frac{\Gamma\vdash\Delta,\varphi;\quad\Gamma\vdash\Delta,\psi}{\Gamma\vdash\Delta,\varphi\land\psi}\quad\frac{\Gamma\vdash\Delta,\varphi,\psi}{\Gamma\vdash\Delta,\varphi\lor\psi}\quad\frac{\Gamma,\varphi\vdash\Delta;\quad\Gamma,\psi\vdash\Delta}{\Gamma,\varphi\lor\psi\vdash\Delta}$$ $$\frac{\Gamma,\varphi\vdash\Delta,\psi}{\Gamma\vdash\Delta,\varphi\rightarrow\psi}\quad\frac{\Gamma\vdash\Delta,\varphi;\quad\Gamma,\psi\vdash\Delta}{\Gamma,\varphi\rightarrow\psi\vdash\Delta}\quad\frac{\Gamma,\varphi\vdash\Delta}{\Gamma\vdash\Delta,\lnot\varphi}\quad\frac{\Gamma\vdash\Delta,\varphi}{\Gamma,\lnot\varphi\vdash\Delta}$$$$\frac{\Gamma,\varphi(t)\vdash\Delta}{\Gamma,\forall x\varphi(x)\vdash\Delta}\quad\frac{\Gamma\vdash\Delta,\varphi(a)}{\Gamma\vdash\Delta,\forall x\varphi(x)}\quad\frac{\Gamma\vdash\Delta,\varphi(t)}{\Gamma\vdash\Delta,\exists x\varphi(x)}\quad\frac{\Gamma,\varphi(a)\vdash\Delta}{\Gamma,\exists x\varphi(x)\vdash\Delta}$$ I see that the formulae above and under the line are equivalent in predicate logic (with some doubt about the meaning of $a$ and $t$) if we read "$;$" as and and if we read the comma as $\land$ when it precedes $\vdash$ and as $\lor$ when it follows it. But I do not see at all how they are a rewriting of the preceding formulae containing $S,\alpha,\alpha_1,\alpha_2, \beta,$... How are they related to them? I have searched very much in the Internet and on books, but I find no information...

Answer 1

The relation between sequent calculus and tableaux method is very well presented in the "little classics" :

• Raymond Smullyan, First-Order Logic (1968).

For the "truth trees" proof procedure, see also :

• Peter Smith, An Introduction to Formal Logic (2003).

You can see also :

• Stephen Simpson, Mathematical Logic (2013).

---

The semantics for sequents, in brief, is the following [see Gaisi Takeuti, Proof Theory (2nd ed - 1987), page 9] :

intuitively a sequent $\gamma_1, \ldots, \gamma_m \vdash \delta_1, \ldots, \delta_n$ means :

"if $\gamma_1 \land \ldots \land \gamma_m$, then $\delta_1 \lor \ldots \lor \delta_n$.

Then we have [page 41] :

A sequent $\Gamma \vdash \Delta$ is satisfied [in an interpretation $\mathfrak I$] if either some formula in $\Gamma$ is not satisfied by $\mathfrak I$, or some formula in $\Delta$ is satisfied by $\mathfrak I$. A sequent is valid it it satisfied in every interpretation.

Thus, the sequent $\gamma_1, \ldots, \gamma_m \vdash \delta_1, \ldots, \delta_n$ is "semantically equivalent" to :

$(\gamma_1 \land \ldots \land \gamma_m) \rightarrow (\delta_1 \lor \ldots \lor \delta_n)$.

---

Regarding specifically the relationship between tableaux and sequent calculus, you can see Smullyan's book; Ch.XI : Gentzen Systems is devoted to explain the "transition" from the first to the second.

Historically Gentzen developer sequent calculus in the '30s and Beth, Hintikka and Smullyan derived from it, in the '50s-'60s, the tableaux method.

The easiest way is to start from tha last one.

It is a "refutation" procedure: it proves $\varphi$ building a refutation tree for $\lnot \varphi$. The tree is built decomposing the root formula according to the rules.

The rules have the nice property [Smullyan, page 25] :

that any immediate extension of a tableau which is true (under a given interpretation) is again true (under the given interpretation). [...] Now a closed tableau $\mathfrak T$ obviously cannot be true under any interpretation, hence [...] the origin of any closed tableau must be unsatisfiable.

Conclusion : if the tableau for $\lnot \varphi$ closes, then $\lnot \varphi$ is unsatisfiable, and thus $\varphi$ is valid (a tautology, if it is a propositional formula).

---

The tableau rules correspond to the sequent calculus rules "read" bottom-up, like in the root-first proof search procedure [see e.g.: Jan von Plato, Elements of Logical Reasoning (2013), page 64-on].

Consider e.g. the connective $\land$; its "signed" rules are :

$$\frac{\displaystyle \frac{\displaystyle T(X \land Y)}{TX}}{TY}\quad\frac{F(X \land Y)}{FX | FY}$$

and compare with the left- and right-rules of sequent calculus :

$$\frac{\Gamma,\varphi,\psi\vdash\Delta}{\Gamma,\varphi\land\psi\vdash\Delta}\quad\frac{\Gamma\vdash\Delta,\varphi\quad\Gamma\vdash\Delta,\psi}{\Gamma\vdash\Delta,\varphi\land\psi}$$

Read the left one ($\land$-left) "bottom-up".

The intended meaning of the rule, according to the above semantics, is that the lower sequent is falsified when "all elements of $\Gamma, \varphi\land\psi$ are true and all element of $\Delta$ are false".

Thus, forgetting about the contexts: $\Gamma, \Delta$, this implies that both $\varphi$ and $\psi$ must be true.

And this, in turn, means that the upper sequent is falsified.

Regarding the right sequent-rule ($\land$-right), the lower sequent is falsified when: "all elements of $\Gamma$ are true and all elements of $\Delta, \varphi\land\psi$ are false".

Forgetting about the "contexts" again, we have that this implies that at least one between $\varphi, \psi$ must be false, and this is the gist of the tableau rule for $F\land$.

This "reading" explains also the peculiar form of axioms in sequent calculus: $A \vdash A$.

With the root-first proof search procedure, the proof ends (positively) when all branches of the "growing tree" reach an axiom.

But, according again to the above semantics, the sequent $A \vdash A$ cannot be falsified, because the condition: "all elements of $\{ A \}$ are true and all elements of $\{ A \}$ are false" will never hold.

This condition is corresponding to the contradiction that allows us to "cross" a branch in a tableau.

Note The peculiarity of sequent rules (in a suitable designed calculus) is that they are, so to say, "hyper sound", i.e. the conclusion is true iff the premises are (this is not so for "traditional" inference rules, like e.g. modus ponens).

---

Regarding the sequent rules for quantifiers, $a$ in $\forall$-right and $\exists$-left is a free variable, with the proviso : $a$ not occurring in $\Gamma, \Delta$.

The $t$ in $\forall$-left and $\exists$-right is a term, with no restrictions.

Intuitively, $\forall$-right is $\forall$-introduction of Natural Deduction : if $\Gamma \vdash \varphi(y)$, then $\Gamma \vdash \forall x \varphi^y_x$, provided that $y$ is not free in $\Gamma$.

$\forall$-left instead, corresponds to $\forall$-elimination of Natural Deduction : if $\Gamma \vdash \forall x \varphi$, then $\Gamma \vdash \varphi^x_t$, where $t$ is a term whatever, substitutable for $x$ in $\varphi$.

---

---

You can see also :

• Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012), Ch.3.2.1 The Relationship Between [Gentzen System] $\mathcal G$ and Semantic Tableaux, page 53-on.