3
$\begingroup$

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...

$\endgroup$
4
$\begingroup$

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

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

You can see also :


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 :

$\endgroup$
  • $\begingroup$ @Self-teachingDavide - see Smullyan, page 106 ... but the little book is "quite compressed", with a lot of results not so easy to be grasped at a first reading. Thus, you have to read it until page 106 ... $\endgroup$ – Mauro ALLEGRANZA Feb 4 '15 at 12:41
  • 1
    $\begingroup$ @Self-teachingDavide . the sequent $γ_1,…,γ_m⊢δ_1,…,δ_n$ is "semantically equivalent" to : $\vdash (γ_1∧…∧γ_m)→(δ_1∨…∨δ_n)$. Thus, truth conditions for $\rightarrow$ apply: it is true when the antecedent is false (and being a conjunction, it is enough that one of $\γ_i$ is false) or when the consequent is true (and being a disjunction, it is enough that one of $\δ_j$ is true). $\endgroup$ – Mauro ALLEGRANZA Feb 5 '15 at 7:12
  • 1
    $\begingroup$ @MauroALLEGRANZA Maybe I'm missing something here: "if some element of $\Gamma$ is false, then all elements of $\Delta, \varphi\land\psi$ must be false" [again, read it as a conditional; thus, if at least one element in $\Gamma$ is false, "reading" it as a conjunction, the antecedent is false; thus in order to satisfy the complete sequent, also the consequent must be false" The fact that the antecedent is false doesn't say anything about the consequent... $\varphi\land\psi\vdash\psi$ doesn't tell us $\neg\left(\varphi\land\psi\right)\vdash\neg\psi$! $\endgroup$ – Hungry May 11 '16 at 8:58
  • 1
    $\begingroup$ @MauroALLEGRANZA We should instead understand ourselves to be supposing the sequent is false the whole time, reading the sequent $\Gamma : \Delta$ as the supposition "every wff in $\Gamma$ is true and every wff in $\Delta$ is false." Tableau rules for T apply to the wffs in $\Gamma$ because they are supposed true the whole time, and the tableau rules for F apply to the wffs in $\Delta$ because they are supposed false the whole time. Reading it this way, we stop at $\varphi : \varphi$ because we've derived a contradiction, just like in a tableau proof. $\endgroup$ – Hungry May 11 '16 at 16:13
  • 1
    $\begingroup$ @Hungry - thanks to your comment, I've corrected the errors. :-) $\endgroup$ – Mauro ALLEGRANZA May 12 '16 at 8:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.