Two forms of Generalization Rule in logic

logicpredicate-logicquantifiers

I have a problem with two forms of the generalization rule in logic.

Shoenfield proves in his book that if $T\vdash\phi$ where $T$ is a set of formulas and $\phi$ is a formula, then $T\vdash\forall x\phi$.

His proof is, "from $T\vdash\phi$ and the tautology $\phi\to(\lnot\forall x\phi\to\phi)$, $T\vdash\lnot\forall x\phi\to\phi$. Then by the $\forall$-introduction rule, $T\vdash\lnot\forall x\phi\to\forall x\phi$ ; so $T\vdash\forall x\phi$ by the tautology $(\lnot\forall x\phi\to\forall x\phi) \to\forall x\phi$" ( The $\forall$-introduction rule can be deduced by the $\exists$-introduction rule which is considered as one of rules of inference in the book).

On the other hand, Enderton shows that if $T\vdash\phi$ and $x$ do not occur free in any formula in $T$, then $T\vdash\forall x\phi$, and says the restriction that $x$ not occur free in $T$ is essential, whereas Shoenfield does not restrict anything.

So $Px\vdash\forall x (Px)$ by Shoenfield and may not by Enderton. I wonder why it happens.

My opinion is that it happens because of the difference between their definition of '$\vDash$ for sets of formulas'. Enderton defines that $Px\vDash\forall x Px$ iff for every structure $\mathfrak A$ and every $a\in A$, the universe of $\mathfrak A$, such that $\mathfrak A\vDash Px[a]$, $\mathfrak A\vDash\forall x Px$. But Shoenfield writes $Px\vDash\forall x Px$ when for every structure $\mathfrak A$ such that $\forall a\in A(\mathfrak A\vDash Px[a])$, $\mathfrak A\vDash\forall x Px$. Obviously, $Px\not\vDash\forall x Px$ with Enderton's definition and $Px\vDash\forall x Px$ with Shoenfield's one.

Are there the others which expain why it happens? and Which definition is used in the modern mathematics?

Best Answer

You are right.

Here is a proof of the "full" Generalization Theorem.

First of all, we can "relax" the $\forall$-Introduction rule (page 31): $A \to B \vdash A \to \forall x B$, provided that $x$ is not free in $A$.

Thus:

  1. $\Gamma \vdash A$

  2. $\vdash A \to (y=y \to A)$ --- it is an instance of a tautology: $y$ new

  3. $\Gamma \vdash y=y \to A$

  4. $\Gamma \vdash y=y \to \forall x A$ --- by "relaxed" $\forall$-Introduction

  5. $\vdash y=y$ --- identity axiom (page 21)

  1. $\Gamma \vdash \forall x A$.

Regarding $\vDash$, there is a difference.

According to Shoenfield (page 20) formula $A$ is a logical consequence of $\Gamma$ if $A$ is valid in every structure in which all formulas of $\Gamma$ are valid.

Consider the case of $(x=0)$ and the structure $\mathbb N$. Formula $(x=0)$ is not valid in it because it is not true that every instance of the formula is true in $\mathbb N$.

If we choose the new constant $c_1$ to name the number $1$, we have that $(x=0)[c_1]$ is false, and thus: $\mathbb N \nvDash (x=0)$.

Thus, "if $(x=0)$ is valid, then $\forall x (x=0)$ is valid" is vacuously true, and thus in Shoenfield's system we have:

$Px \vDash \forall Px$,

and this is consistent with the "unrestricted" Generalization rule:

For any $\Gamma$ and any $A$, if $\Gamma \vdash A$, then $\Gamma \vdash (∀x)A$.

See Tourlakis, page 43 and page 52.

In a nutshell, for Shoenfield $Px$ and $\forall x Px$ are semantically equivalent. This is not so in Enderton's system.

This fact induces some other differences: in Enderton, thanks to the restriction on Generalization, we have an "unrestricted" Deduction Theorem, while in Shoenfield and Tourlakis we have that "for any closed formula $A$ and arbitrary formula $B$, if $\Gamma, A \vdash B$, then $\Gamma \vdash A → B$."

In both cases, what is avoided is to "validate" the invalid: $Px \to \forall x Px$.

In Enderton's system the "move" $Px \vdash \forall x Px$ is not allowed.

In Shoenfiled's system we have it but we cannot use DT to derive $Px \to \forall x Px$.

See also this post as well as this one.

Related Question