Unable to prove this simple inference using sequent calculus

Question

In a recent question, I asked if the folowing inference is valid provided that the variable $z$ does not occur free in $\Gamma$ (Note: No restriction regarding whether or not $z$ occurs free in $\phi$ is assumed) :

$${ \Gamma \vdash \phi \over \Gamma \vdash \forall z.\phi }$$

One respondent, of high repute ($\simeq$ 25k), commented that it is.

Although, intuitively this inference seems valid, I have been unable to derive it proceeding from the rules of inference commonly given for sequent calculus (predicate logic version).

Assuming that all of the commonly given accounts of sequent calculus are sound and complete, shouldn't I be able to prove any valid formula/inference from their axiom(s) and rule(s) of inference?

Can any one offer a proof of the abovementioned inference that proceeds from the axiom(s) and rule(s) of inference of a sequent calculus?

Answer 1

You can see in :

• Gaisi Takeuti, Proof Theory (2nd ed - 1987), page 10, the quantifiers rules for sequent calculus :

$${ \Gamma \to \Delta, \ F(y) \over \Gamma \to \Delta, \ \forall xF(x) } (\forall \text {-right})$$

where $y$ does not occur in the lower sequent.

Being one of the "primitive" rule of the sequent calculus, it is enough to consider $\Delta = \emptyset$ in the $(\forall$-right) rule and we have the requested inference.

In this case, the restriction on $y$ not free in the lower sequent, amounts to $y$ not free in $\Gamma$ nor in $F$.

---

The rule corresponds to the $\forall$-introduction rule of natural deduction :

$${ A(y/x) \over \forall xA } (\forall \text {I})$$

The rule of universal introduction has the variable restriction that $y$ must not occur free in any assumption that $A(y/x)$ depends on nor in $\forall xA$. [...] The variable restriction guarantees that $y$ stands for an "arbitrary individual" for which $A$ holds, which is the direct ground for asserting the universal proposition.

See : Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 64.

---

Both proof systems need the restriction on the so-called eigenvariable $x$ of the rule, in order to avoid proving invalid formulae.

Consider the following counter-example, assuming $\Gamma = \{ x = 0 \}$ and $\Delta = \emptyset$.

Clearly :

$x=0 \vdash x=0$

and thus, if we disregard the restriction, we can conclude with :

$x=0 \vdash \forall x(x=0)$.

But both natural deduction and sequent calculus have no restrictions on the "deduction theorem" (i.e. the rules $\to$-introduction and $\Rightarrow$-right, respectively) and thus, from the above deduction, we can infer the invalid :

$\vdash (x=0) \to \forall x(x=0)$.

---

---

In :

• Heinz-Dieter Ebbinghaus & Jörg Flum & Wolfgang Thomas, Mathematical logic (2nd ed 1994)

there is a "weird way" to present sequent calculus. The quantifier $\forall$ is primitive in the syntax [see page 16] but the rules of the calculus regarding it are all "derived".

In order to do this, we have to supplement the calculus with the "usual" equivalence between $\forall$ and $\lnot \exists \lnot$.

If so, we have the following derivation :

0) $\Gamma \ \ \varphi$ --- premise

1) $\Gamma \ \ \alpha \ \ \varphi$ --- for some $\alpha \in \Gamma$

2) $\Gamma \ \ \lnot \varphi \ \ \lnot \alpha$ --- (Cp) [contraposition, page 64]

3) $\Gamma \ \ \exists x \lnot \varphi \ \ \lnot \alpha$ --- 5.1(b) [page 68 : here we need the restriction on $x$ not free in $\Gamma, \alpha$

4) $\Gamma \ \ \lnot \lnot \alpha \ \ \lnot \exists x \lnot \varphi$ --- (Cp)

5) $\Gamma \ \ \alpha \ \ \lnot \exists x \lnot \varphi$ --- 3.6(a1) [page 65 : double negation]

6) $\Gamma \ \ \lnot \exists x \lnot \varphi$ --- $\alpha \in \Gamma$

7) $\Gamma \ \ \forall x \varphi$ --- from 6) by equivalence of $\lnot \exists \lnot$ and $\forall$ : $x$ not free in $\Gamma$.

---

You can compare with :

• Wolfgang Rautenberg, A Concise Introduction to Mathematical Logic (3rd ed - 2010),

that has a similar "austere" presentation of sequent calculus.

$\forall$ is primitive and the rules for quantifiers [page 92; see also page 79] are : $\forall$-elimination ($\forall1$) and $\forall$-introduction :

$${ X \vdash \alpha^y_x \over X \vdash \forall x \alpha } \ (\forall 2)$$

with $y \notin \text {free} X \cup \text {var} \alpha$.

The rules for $\exists$ are derivable [see Exercise 1, page 97].

In this case, it is explicitly said [page 56] that :

Other logical symbols serve throughout merely as abbreviations, namely $∃x \alpha := ¬∀x¬ \alpha$, [...].

Note : the symbol $\varphi^y_x$ stands for [see page 59] the formula that results from replacing all free occurrences of $x$ in $\varphi$ by $y$.