1
$\begingroup$

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?

Improve this question
$\endgroup$
  • $\begingroup$ I think that part of the misunderstanding is in the use of the "eigenvariable" in the rule. In your "form", of course we cannot impose the restriction $z$ not free in $\Gamma$ and $\phi$, because in this case the quantification on $z$ is quite useless. In this case, we impose that $z$ is not free in $\Gamma$. The "purist" formulation (see Takeuti) separates symbols for free and bound variables; in this case we start with $\phi(y)$ and move to $\forall z \phi(z)$. Now the restriction is that the variable in the scope of the quantifier (i.e. $z$) must not be free in $\Gamma$ nor in $\phi$. $\endgroup$ – Mauro ALLEGRANZA Mar 29 '15 at 13:08
3
$\begingroup$

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 :

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

Improve this answer
$\endgroup$
  • $\begingroup$ Let $\mathscr{I}$ denote the inference stated in my original question. I feel $\mathscr{I}$ is of a nature that is not readily amenable to the inference rule $(\forall \text {-right})$ you gave. With regard to $\mathscr{I}$, let $\Gamma \equiv \{ x = 0 \}$ and $\phi \equiv (x = 0)$. Then, since $\{ x = 0 \} \vdash (x = 0)$ is valid, we see that $\Gamma \vdash \phi$ is valid. Also, since $\{ x = 0 \} \vdash \forall z.(x = 0)$ is valid, we see that $\Gamma \vdash \forall z.\phi$ is valid. Thus, $\mathscr{I}$ holds even though $x$ occurs free in $\Gamma$. $\endgroup$ – memexor Mar 28 '15 at 20:14
  • $\begingroup$ Also, whilst I agree with the $\forall$-introduction rule of natural deduction that you gave, it too addresses a situation that is very different to the original inference stated in my question. The original inference stated in my question is 'quite happy' for the eigenvariable (or any other variable) of the upper sequent's consequent to occur free in $\Gamma$. Can you see that the original inference stated in my question is of a nature not readily amenable to the inference rule $(\forall \text {I})$ that you gave? $\endgroup$ – memexor Mar 28 '15 at 20:17
  • $\begingroup$ Just to clarify ... The inference stated in my original question makes no assumptions about (i.e. places no restrictions on) the relationship between the occurrences of variables in $\phi$ (free or bound) and the occurrences of variables in $\Gamma$ (free or bound). The only restriction assumed by the inference stated in my original question, is that the quantifier variable $z$ in the lower sequent's consequent does not occur free in $\Gamma$. $\endgroup$ – memexor Mar 28 '15 at 20:37
  • $\begingroup$ The inference stated in my original question does not assert that $\Gamma \vdash \forall x \phi$ can be inferred from $\Gamma \vdash \phi$ irrespective of x being free in $\Gamma$ or not. The inference stated in my original question explicitly restricts the quantifier variable of the lower sequent's consequent to being one that does not occur free in $\Gamma$. $\endgroup$ – memexor Mar 28 '15 at 20:47
  • 1
    $\begingroup$ Mauro and @Sebastian ... I'd like to reward you both for your high quality inputs to the analysis of this topic. One way, that comes to mind, is for Sebastian to answer the related question by citing the presence of the concerned inference in the Ebbinghaus book (5.5 b4) ... That would ensure that readers know that it's a correct inference, and I could then accept Sebastian's answer there, whilst accepting Mauro's answer here (end result ... both of you are rewarded for your efforts). Does that seem reasonable? $\endgroup$ – memexor Mar 31 '15 at 21:52

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.