# mathematical logic: a step is not clear

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.

-

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.

-

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$$
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"). –  Henning Makholm 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