3

I'm currently taking an introductory course in Mathematical logic(prerequisites is only advanced calculus) and my lecture notes are based on Enderton's book 'Mathematical Introduction to Logic'

Suppose $\varphi$ is deducible from $\Gamma$ and we are seeking a proof of this fact. There are several cases, one of the which is $\varphi=\forall x \psi$. According to the book, if $x$ should occur free in $\Gamma,$ there will be a variable $y$ such that $\Gamma \vdash \forall y \ \psi ^{x}_{y}$ and $\forall y \ \psi^{x}_{y} \vdash \forall x \ \psi.$

May I know how do we prove that there will be a variable $y$ such that $\Gamma \vdash \forall y \ \psi ^{x}_{y}$ and $\forall y \ \psi^{x}_{y} \vdash \forall x \ \psi \ ?$ The author then refers one to Re-replacement lemma but I can't see how are both related. Could anyone instruct me please?

Thank you.

Alexy Vincenzo
  • 5,400
  • Can you give us the info for the page of Enderton's book where to locate the proof ? Re-replacement lemma [page 130] says that (roughly speaking) with free vars the "change" of $x$ with $y$ and back, in general, is not correct, because the "reverse" operation do not restore the original formula. Think to $\varphi := x=y$; with $\varphi^{x}{y}$ we will have $\varphi' := y=y$ and with $\varphi'^{y}{x}$ we will have $\varphi'' := x=x$, which is not the original one. – Mauro ALLEGRANZA Mar 27 '14 at 08:52
  • @MauroALLEGRANZA: Thanks for reply. I'm referring to pg120. Also, could you advise me on how to prove Re-replacement lemma on pg130(Qn9b) > – Alexy Vincenzo Mar 27 '14 at 09:57
  • 1
    About Re-replacement lemma on page 130, Ex.9 (b) : Show that if $у$ does not occur at all in $\varphi$, then $x$ is substitutable for $y$ $\varphi^{x}{y}$ and $(\varphi^{x}{y})^{y}_{x}=\varphi$ (hint: use induction on $\varphi$) the proof works by induction according the formation rules for formulae (page 74-on) : (i) if $\varphi$ is atomic without $y$ you cannot put $x$ in place of it: so, nothing change and the "double subst" gives you $\varphi$; (ii) with connectives, you use the induction hypo: if it works e.g. for $\alpha$ and $\beta$, it will works also for $\alpha \land \beta$. 1/2 – Mauro ALLEGRANZA Mar 27 '14 at 10:20
  • 1
    (iii) the last case take care of quantifiers; consider $\forall$ and let $\varphi := \forall z \psi$. If $y$ does not occur in $\varphi$, for sure $y \ne z$ and there is no quantifier $\forall y$ in $\psi$; thus, effecting the subst into $\psi$, there is no danger that $y$ get captured by a quantifier inside $\psi$, altering the meaning of the formula. 2/2 – Mauro ALLEGRANZA Mar 27 '14 at 10:26
  • The matter seem obscure but you must re-read the comments by Enderton. (i) page 117 : "The generalization theorem reflects our informal feeling that if we can prove '- - x - -' without any special assumptions about $x$, we then are entitled to say that 'since $x$ was arbitrary, we have $\forall x$ - - x - -' ". (ii) "the foregoing examples illustrate a sort of interchangeability of constant symbols with free variables. This interchangeability is the basis for the following variation on the generalization theorem [i.e.Th 24F (Generalization on Constants)]". 1/2 – Mauro ALLEGRANZA Mar 27 '14 at 11:30
  • (iii) page 123 : with Corollary 24G, we use a "generic" constant in place of the variable $x$ in $\varphi$. If this constant $c$ does not occur in the assumption $\Gamma$ of the proof, it "works like" a variable; thus, we may "generalize" on it. 2/2 – Mauro ALLEGRANZA Mar 27 '14 at 11:41
  • Comment about page 120: 2. Suppose that $\varphi$ is $\forall x \psi$. If $x$ does not occur free in $\Gamma$, then it will suffice to show that $\Gamma \vdash \psi$ (Even if $x$ should occur free in $\Gamma$, the difficulty can be circumvented. There will always be a variable $у$ such that $\Gamma \vdash \forall y \psi[x/y]$ and $\forall y \psi[x/y] \vdash \forall x \psi$). Comm. (i) $x$ must not be free in $\Gamma$ because otherwise, with $\Gamma = { \alpha(x) }$ we may have $\alpha(x) \vdash \forall x \alpha(x)$, and this in not sound (are you able to find a counterexample ?). 1/2 – Mauro ALLEGRANZA Mar 27 '14 at 16:38
  • (ii) Even if $x$ should occur free in $\Gamma$, the difficulty can be circumvented: we have at our disposal an infinite supply of ind var $x_i$. A derivation is a finite sequence of formulae; thus, it may use at most a finite number of variables, and we are always able to find a "new" one not already used in the proof. 2/2 – Mauro ALLEGRANZA Mar 27 '14 at 16:41
  • @Mauro ALLEGRANZA: Thanks for the detailed response. For the last case of the induction proof(to the Re-replacement lemma), where $\varphi:=\forall z \ \psi$ does not contain $y,$ so $\psi$ does not contain $y.$ Suppose $x\neq y,$ then $(\forall z \ \psi)^{x}{y}=\forall z(\ \psi^{x}{y})$ and so $((\forall z \ \psi)^{x}{y})^{y}{x}=\forall z((\psi)^{x}{y})^{y}{x} = \forall z \ \psi,$ where the last step follows from induction hypothesis applied on $\psi$. Is my argument correct? – Alexy Vincenzo Apr 03 '14 at 06:42
  • Basically, if $\varphi$ does not contain $y$, as you say, also $\psi$ does not. Thus, basically, we have "nothing to calculate" : the double substitution does not act on $\psi$, so does not act on $\varphi$. – Mauro ALLEGRANZA Apr 03 '14 at 12:01

1 Answers1

4

I suppose that you are working with Corollary 24G, page 124, of Herbert Enderton, A Mathematical Introduction to Logic (2nd ed Harcourt - 2001) :

Assume that $\Gamma \vdash \varphi^{x}_{c}$, where the constant symbol $c$ does not occur in $\Gamma$ or in $\varphi$. Then $\Gamma \vdash \forall x \varphi$, and there is a deduction of $\forall x \varphi$ from $\Gamma$ in which $c$ does not occur.

The proof invoks Theorem 24F (Generalization on Constants) [page 123].

The motivation of the Corollary is [page 124] : "We want to apply Theorem 24F in circumstances in which not just any variable will do. In the following version, there is a variable $x$ selected in advance."

From the hypotheses $\Gamma \vdash \varphi^{x}_{c}$, where the constant symbol $c$ does not occur in $\Gamma$ or in $\varphi$, Theorem 24F gives us a deduction (without $c$) from $\Gamma$ of $\forall y ((\varphi^{x}_{c})^{c}_{y})$ where $y$ does not occur in $\varphi^{x}_{c}$.

But since $c$ does not occur in $\varphi$,

$((\varphi^{x}_{c})^{c}_{y}) = \varphi^{x}_{y}$.

This substitution works, because there are no occurrences of $c$ in the "original" formula $\varphi$; thus, substituting $c$ in place of $x$, and then $y$ in place of $c$, we do not have "unpleasant effects".

Thus, we may conclude that :

$\Gamma \vdash \forall y \varphi^{x}_{y}$ --- (a).

The last step in the proof is to show that :

$\forall y \varphi^{x}_{y} \vdash \forall x \varphi$.

To do this, he invokes Axiom 2 [see page 112] : $\forall y \alpha \rightarrow \alpha^{y}_{t}$.

With $\varphi^{x}_{y}$ in place of $\alpha$ and $x$ in place of $t$, we have as $\alpha^{y}_{t}$ the result $(\varphi^{x}_{y})^{y}_{x}$ , i.e. $\varphi$.

The proof now call for a formal verification through Re-replacement lemma.

Having verified this, we have $\vdash \forall y \varphi^{x}_{y} \rightarrow \varphi$.

Then the following generalization is also an axiom [see page 112] :

$\vdash \forall x (\forall y \varphi^{x}_{y} \rightarrow \varphi )$.

By Axiom 4 ($x$ is not free in $\forall y \varphi^{x}_{y}$), we have :

$\vdash \forall y \varphi^{x}_{y} \rightarrow \forall x \varphi$.

Thus, from (a) above, we may finally conclude :

$\Gamma \vdash \forall x \varphi$.

Mauro ALLEGRANZA
  • 94,169