# translation of a sentence in FOL using Skolem functions

Consider the first-order sentence

(1) $\forall x\exists y(\forall z Dxz\to\exists z\neg Dyz)$

and interpret Dab as the two-place relation "a has doubts about b." On a recent exam, I translated the sentence back into English as

(2) For everyone who has doubts about everything, there's someone who doesn't have doubts about something.

(3) Even if there is someone who has doubts about everything, there is still someone who does not have doubts about something.

But I can't see how these two translations come apart -- i.e. I can't think of a model where one is true but the other is false. What am I missing?

Let me elaborate just a bit. (3) is certainly the best translation of (1) after it has been transformed into what Quine called "pure form": by the laws of quantifier passage, (1) is equivalent to

(1') $\exists x\forall z Dxz\rightarrow \exists y\exists z\lnot Dyz$

But with (2) I was trying to expose the general dependency, in the manner of Skolem functions, of the existentially quantified y on the universally quantified x. I grant that there's a reading of (2) according to which I'm asserting that for every person who has doubts about everything there's a unique person who doesn't have doubts about something (a much stronger claim than (1)), but it seems to me that (2), on the face of it, doesn't require this reading -- it doesn't say outright that y=f(x) is injective and indeed is consistent with it being constant.

So my question is really aimed at logic instructors. Would you have counted off if I offered this translation, and if so, why? The best explanation I can see is that (2) is ambiguous with its most natural reading being the stronger reading I explained above. Or if I really am missing something here, please point it out.

Thanks!

-
My best guess would be that the problem was indeed the reading that there are at least as many people who don't have doubts about something as people who have doubts about everything, as in "for every Fermat liar there is a Fermat witness". – joriki Apr 25 '12 at 3:27
Don't you know that FOL using Skolem functions has been superseded by LOL using keypad functions? – Gerry Myerson Apr 25 '12 at 4:32