2

I refer to Stephen Cole Kleene, Mathematical Logic (1967 - Dover reprint : 2002).

At pag.108 he introduces the definiton of deducible from assumptions (in Predicate Calculus) with restrictions regarding the use of the $\forall$-rule :

"from $C \rightarrow A(x)$ to $C \rightarrow \forall x A(x)$" ($x$ not free in $C$) ,

on the vars that are free in the assumptions.

At pag.109 [Example 9] he makes the example of a (correct) deduction of $R \rightarrow \forall x P(x)$ from $\forall y (R \rightarrow P(y)$). From steps 5 and 6 in the deduction, we understand that y is not free in R (he applies $\forall$-rule with y).

At pag.110 he makes some comments on the restrictions on free vars and adds that :

we are not justified in saying $"R \rightarrow P(y) \vdash R \rightarrow \forall x P(x)"$. In fact, this is not true, since [by soundness and ref.to previous Exercise 20.2a (pag.107 - there is a misprint : the text has "Example"), is not the case that] $"R \rightarrow P(y) ⊨ R \rightarrow \forall x P(x)"$ were true.

But why we cannot simply justify $R \rightarrow P(y) \vdash R \rightarrow \forall y P(y)$ by the $\forall$-rule ? I think that the change in the bound variable is (as Kleene says in the same lines) is immaterial.

Added Dec,2 : The deduction $R \rightarrow P(y) \vdash R \rightarrow \forall y P(y)$ is not correct according to Kleene's definition [pag.108] of deduction (from assumptions) with all free variables held constant.

The correct interpretation of the $\forall$-rule is [see also Th.16, pag.96] :

"if $\vdash C \rightarrow A(x)$ then $\vdash C \rightarrow \forall xA(x)$" (x not free in $C$),

and not : "$C \rightarrow A(x) \vdash C \rightarrow \forall xA(x)$".

If we apply the $\forall$-rule to the assumption $C \rightarrow A(x)$ , we have the one-step deduction : $C \rightarrow A(x) \vdash ^x C \rightarrow \forall xA(x)$ (x varied), because x is not free in the assumption.

Mauro ALLEGRANZA
  • 94,169

2 Answers2

2

I don't have the book with me but the answer should be something along these lines:

Consider $P(y):=\exists{x} (x\neq{y})$. Let $R$ be the set of logical axioms along with $\exists{x_{1},x_{2} (x_{1}}\neq{x_{2}})$ and $P(y)$. Then for any $M\models{R}$, we have $M\models{\forall{y}P(y)}$. But then if we didn't have restrictions we would end up with $\exists{x} (x\neq{x})$ which is absurd. So in order to make things work out we need restrictions. Different authors impose different rules to get around such problems.

Also while it is true that here we have $M\models{\forall{y}P(y)}$, in this case it is not the same as saying $M\models{\forall{x}P(x)}$ and that is what I think Kleene is trying to point out.

UserB1234
  • 2,198
  • Regarding your first comment, I agree that the restrictions are imposed in order to avoid wrong conclusions. Reading again Kleene's text, now I'm thinking that I've made a mistake : I cannot simply justify $R \rightarrow P(y) \vdash R \rightarrow \forall y P(y)$ by the $\forall$-rule because in this way I should violate the restriction about the use of A-rule with free vars in assumption. Regarding your second comment, I still thinking that $\forall x P(x)$ and $\forall y P(y)$ are the same. – Mauro ALLEGRANZA Nov 24 '13 at 16:30
  • They are not the same. $P(x)=\exists{x}(x\neq{x})$. So $\forall{x}P(x)=\forall{x}\exists{x}(x\neq{x})$. Since all the $x$'s are bound to the existential quantifier the above gives $\forall{x}P(x)=\exists{x}(x\neq{x})$ which is absurd (or your theory is inconsistent to begin with). – UserB1234 Nov 24 '13 at 19:53
  • You seem to be getting things mixed up. Naively both the statements seem to say the same thing. But they do not. This is the reason why books spend so much time formulating and proving results from a bunch of rules. In the example $\forall{w}P(w)$, $\forall{z}P(z)$ will all be valid conclusions; just not $\forall{x}P(x)$ (so your intuition works for those just not for $\forall{x}P(x)$). Also in the example $R\vdash{\forall{y}P(y)}$. This follows because for any $M\models{R}$ and $a\in{M}$ we have $b\in{M}$ such that $M\models{a\neq{b}}$. So you don't have to worry about rules there. – UserB1234 Nov 24 '13 at 20:17
1

After reading Kleene I believe now I can completely address the question. So I hope the following answer can add some details to the one above.

For start let's say that you have misread the $\forall$-rule, indeed as stated in Kleene's book the rule should be read as

If $\ \vdash R \rightarrow P(x)$, where $R$ doesn't contain a free occurrence of $x$, then $\vdash R \rightarrow \forall x P(x)$.

The point is that the rule require that you have to deduce that $R \rightarrow P(x)$ is valid without any assumption. Actually you could strengthen a little bit such rule using the rule

If $R \vdash P(x)$, where $R$ doesn't contain any free occurrence of $x$, then $R \vdash \forall x P(x)$

Adding one of such rules to the propositional calculus (and the axioms of the predicative calculus) provide always the same system.

The reason why we don't want the rule $\vdash R \rightarrow P(x)$ then $\vdash R \rightarrow \forall x P(x)$ is that we would like to have the soundness property for the predicate calculus:

For every pair of formulas in the predicate calculus $A$ and $B$ if $A \vdash B$ then $A \models B$.

This theorem basically states that whenever we derive through the application of the system rules a judgment of the form $\Gamma \vdash A$ we have that in the semantics the judgment $\Gamma \models A$ holds. And this is the minimal property we require for every logical system.

Since with the semantics of first order calculus given in Kleene's book is not possible to prove such a statements as

$$R \rightarrow P(y) \models R \rightarrow \forall x P(x)$$

it follows that if we wish to have a sound system we cannot add the rule

If $R \rightarrow P(y) \vdash R \rightarrow \forall x P(x)$

to the calculus. Using the weaker rule of the system you can deduce the soundness theorem and that implies that the stronger rule above cannot hold in the logical system.

Hope this helps.

Giorgio Mossa
  • 18,150
  • Thanks ! I suppose that the same reason applies to the difference between the Strong form of the Gen rule : $A(x) \vdash \forall xA(x)$ and the Weak form of it : if $\Gamma \vdash A(x)$ then $\Gamma \vdash \forall xA(x)$. – Mauro ALLEGRANZA Nov 25 '13 at 15:20
  • @MauroALLEGRANZA Indeed: you can obtain the form $A(x) \vdash \forall x A(x)$ as an instance of $\Gamma \vdash \forall x A(x)$ when considering $\Gamma = {A(x)}$. – Giorgio Mossa Nov 25 '13 at 15:26
  • Now I'm again confused... putting $\Gamma = A(x)$ I will have the Strong Gen : $A(x) \vdash \forall xA(x)$, but violating the proviso : x not free in $\Gamma$. – Mauro ALLEGRANZA Nov 25 '13 at 15:35
  • What I can obtain (I think correctly) putting $\Gamma = \emptyset$ is : if $\vdash A(x)$ then $\vdash \forall xA(x)$. – Mauro ALLEGRANZA Nov 25 '13 at 15:42
  • My apologize, I should have been more precise. What I meant is that if you use the stronger (wrong) form of the rule, namely $\Gamma \vdash A(x)$, where $\Gamma$ can contain formulas that have free occurrence of $x$, then you can deduce the judgment $A(x) \vdash \forall x A(x)$, which would violate the soundness condition. – Giorgio Mossa Nov 25 '13 at 15:55
  • That's why we need to add the requirement that the formulas in $\Gamma$ have to not contain any free occurrence of $x$. @MauroALLEGRANZA – Giorgio Mossa Nov 25 '13 at 15:57