Elliott Mendelson, Introduction to Mathematical Logic – Gen-rule and logical consequence

In Stephen Cole Kleene, Mathematical Logic (1967 – Dover reprint : 2002) there is a counterexample to the rule : $”A(x)\vdash\forall xA(x)”$.

The counterexample is (pag.110):

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, is not the case that] $”R \rightarrow P(y) \vDash R \rightarrow \forall x P(x)”$ were true.

Elliott Mendelson, Introduction to Mathematical Logic (4th ed – 1997) uses the generalization rule; trying the same example in Mendelson’s system, we have :

1) $R \rightarrow P(y)$ — assumption

2) $R$ — assumption

3) $P(y)$ — 1,2 MP

4) $\forall yP(y)$ — 3,Gen

5) $R \rightarrow \forall yP(y)$ — 2,4 by Deduction Th ($y$ not free in $R$)

Is it correct ? Of course, I cannot have : $\vdash (R \rightarrow P(y)) \rightarrow (R \rightarrow \forall yP(y))$ because now $y$ is free in $R \rightarrow P(y)$ and so DT does not apply.

May I say that this is acceptable in Mendelson’s system because in it the deducibility relation ( $\vdash$) tracks validity and not logical consequence (according to Mendelson definition) ?

Solutions Collecting From Web of "Elliott Mendelson, Introduction to Mathematical Logic – Gen-rule and logical consequence"

I think that the correct answer needs a careful comparison of Kleene’s system [Mathematical Logic, 1967] and Mendelson’s one [Introduction to Mathematical Logic, fourth ed, 1997], regarding the relation, in the respective systems, between the two notion of consequence : the syntactical one ($\vdash$) and the semantical one ($\vDash$).

First of all, both authors define in the same way “validity” and “logical consequence”.

In Kleene’s system the “basic” quantifier rule is the $\forall$-rule [see Th.16, pag.96] :

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

According to Kleene’s remark [pag.110],

we are not justified in saying $”R \rightarrow P(y) \vdash R \rightarrow \forall x P(x)”$. In fact, this is not true, since [is not the case that] $”R \rightarrow P(y) \vDash R \rightarrow \forall x P(x)”$ were true.

This counterexample shows that we are not licensed to read the $\forall$-rule as :

$C\rightarrow A(x) \vdash C \rightarrow \forall xA(x)$.

Accordingly, Kleene’s system derives the (weak) Gen-rule : “if $\vdash A(x)$ then $\vdash \forall xA(x)$”, where the strong one : “$A(x) \vdash \forall xA(x)$” is not allowed (because unsound).

In Mendelson’s system, instead, Gen-rule is the strong one : “$A(x) \vdash \forall xA(x)$”, so that the above derivation is correct; in Mendelson’s system we have that :

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

(but, of course, not $\vdash (R \rightarrow P(y)) \rightarrow (R \rightarrow \forall x P(x))$, due to the restrictions of the Deduction Theorem).

The main difference between the two systems is that in Kleene’s book we have that :

$A \vdash B$ iff $A ⊨ B$.

This is not true , in general, for Mendelson’s system; in it we have (for example) :

$P(x) \vdash \forall xP(x)$ , by Gen,

but not : $P(x) \vDash \forall xP(x)$ ,

by the “usual” counterexample [the domain of the interpretation is the set of natural numbers, the interpretation of $P$ is the property “is even” and take as assignement to the free variable $x$ the number $2$].

See also George Tourlakis, Lectures in Logic and Set Theory, Volume 1 : Mathematical Logic [2003], pag.50 (footnote) :

In Mendelson (1987) $\vDash$ is defined inconsistently with $\vdash$.