1
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ $\exists$-introduction rule is " if $x$ do not occur free in $\phi$, infer $\exists x\psi\to\phi$ from $\psi\to\phi$". $\endgroup$ – dre rt Jan 21 at 5:26
  • $\begingroup$ I have found it useful to associate each universal generalization (Intro A) with the discharging of a premise so as to eliminate any free variables introduced by that premise and by any subsequent statements. I introduce new free variables only by premise or existential specification (Elim E), not by universal specification (Elim A).The only free variables remaining in the resulting universal generalization would have been introduced prior to the premise being discharged. It seems to me that this is what mathematicians habitually do in informal proofs. It works. $\endgroup$ – Dan Christensen Jan 21 at 15:42
  • $\begingroup$ It also helps to make the domain of quantification explicit for every quantifier, as is usually done in most mathematical proofs. $\endgroup$ – Dan Christensen Jan 21 at 15:54
1
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ At the beginning of chapter 3, Shoenfield says that a theory $T$ is fixed and he will examine some of the theorems which can be proved in $T$, so I think the generalization rule proved by Shoenfield's system is actually " if $T\vdash\phi$ then $T\vdash\forall x\phi$". $\endgroup$ – dre rt Jan 21 at 7:23
  • $\begingroup$ And in page 6, he says that when no confusion results, he omits the $T$ in "$T\vdash$". $\endgroup$ – dre rt Jan 21 at 7:32
  • $\begingroup$ Shoenfield defines a theory to be a formal system(please see page 22) and I think that "if $T\vdash\phi$ then $T\vdash\forall x\phi$" can be deduced by the proof of Shoenfield in page 31. Am I wrong? $\endgroup$ – dre rt Jan 21 at 7:43
  • $\begingroup$ I wrote in the above question "where $T$ is a set of formulas", but it can be understood as "where a formal system $T$ has nonlogical axioms which are formulas" $\endgroup$ – dre rt Jan 21 at 8:00
  • $\begingroup$ "if $\phi$ can be proved in $T$ whose nonlogical axioms are formulas, then $\forall x\phi$ can be also proved in $T$" is proved in page 31. I think that it is because of Shoenfiled's formulation of syntax, rules of inference. See Chang and Keisler model theory which take the rule "from $\phi$ infer $\forall x\phi$" as rules of inference. $\endgroup$ – dre rt Jan 21 at 8:29

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.