3

I'm reading the Shoenfield's book Mathematical Logic. On page 53 it states:

Let r be the special constant for $\exists x.\neg$A. Then $\exists x. \neg A \implies \neg A_x[\boldsymbol{r}]$ [substitution of r for x] is an axiom of $T_c$. Bringing the left-hand side to prenex form and using the tautology theorem,

$$⊢_{T_c} A_x[\boldsymbol{r}] \implies\forall x. A.$$

I do not understand why the author refers to prenex form. Someone can explain? Thank you.

Community
  • 1
Bento
  • 554
  • 3
  • 11

2 Answers2

1

But why does Shoenfield seemingly refer to the first move as "Bringing the left hand side into prenex form"? The left-side is in prenex form already. The operation of dragging the negation of the front Is not making it prenex (by his own standards).

I agree completely. I think he actually wanted to write something like: "Bringing the left side to the step precedeing the prenex form [i.e. the inversion of prenex operation (b) on page 37, and assuming, with this, the opening of A - see in this respect the use of the theorem (1) in relation to an open formula in the following Herbrand's theorem]".

A mystery why he writes that?

Of course, the mystery will not be solved by the author, since he's gone.

Bento
  • 554
  • 3
  • 11
0

[Corrected version, after comments!]

Evidently $\exists x \neg A \to \neg A_x[\mathbf{r}]$ is an axiom. Bring the quantifier to the front on the l.h.s. and we have $$\vdash_T \neg \forall x A \to \neg A_x[\mathbf{r}]$$ and contraposing (which we allowed to do by "using the tautology theorem") we get $$\vdash_T A_x[\mathbf{r}] \to \forall x A$$

But why does Shoenfield seemingly refer to the first move as "bringing the left hand side into prenex form"? The left-side is in prenex form already. The operation of dragging the negation of the front isn't making it prenex (by his own standards). A mystery why he writes that?

Peter Smith
  • 54,743
  • I think it's confusing because $\exists x \neg A$ looks more prenex to me than $\neg \forall x A$ does. (But I suppose one could define "prenex" to mean "formula begins with a string of $\neg$ and $\forall$ and is otherwise quantifier-free", where I'm used to "formula begins with a string of $\exists$ and $\forall$ and is otherwise quantifier-free"). – hmakholm left over Monica Oct 28 '12 at 21:15
  • I received this observation also:

    I think he may have in mind just the negation Bringing out through the sign exists (this is what you do When proving prenex normal form) and then deducing the contrapositive.

    I too had thought of this, but the exposition of the text is not clear (literally, "prenex form" refers to an entire formula: those who say that *A* is prenex?)

    In addition, according to the definition of the book, "prenex form" is when there is only a prefix consisting of only quantifiers: thus $\neg$$\forall x A$ does not fall into that category.

     – Bento Oct 28 '12 at 21:58
  • I received this observation also:

    I think he may have in mind just bringing the negation out through the sign exists (this is what you do when proving prenex normal form) and then deducing the contrapositive.

    I too had thought of this, but the exposition of the text is not clear (literally, "prenex form" refers to an entire formula: those who say that *A* is prenex?)

    In addition, according to the definition of the book, "prenex form" is when there is only a prefix consisting of only quantifiers: thus $\neg$$\forall x A$ does not fall into that category.

     – Bento Oct 28 '12 at 22:08
  • I forgot to thank you very much for your reply and comments. – Bento Oct 28 '12 at 22:15
  • Oooops I really really wasn't concentrating in my initial answer there -- taking my eye of the ball because of the misplaced negations in the uncorrected version?? Henning is quite right, I misused "prenex". But then it seems that Shoenfield did too, given what he says earlier now I've checked. – Peter Smith Oct 28 '12 at 23:11