Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
add comment

2 Answers

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.

share|improve this answer
add comment

[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?

share|improve this answer
    
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
    
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.