2

I do not understand the application of the "axiom of choice " in the proof of equisatisfiability of Skolem form.

Can you help show me the understandable format in this case ?

Here is the proof from wiki https://en.wikipedia.org/wiki/Skolem_normal_form in the part "Correctness of Skolemization may be shown on the example formula..."

Sorry about that I am using Chrome and can not just paste all the text here.

gymbvghjkgkjkhgfkl
  • 8,090
Keith
  • 165
  • you're choosing a choice function on the indexed family $({ y \mid R(x_1,\ldots, x_n,y)})_{x_1,\ldots, x_n}$ – Hayden Mar 07 '17 at 14:28

2 Answers2

6

Suppose I want to show that "$\forall x\exists yP(x, y)$" is equivalent to "$\exists F\forall x P(x, F(x))$". One direction (from right to left) is trivial; in the other direction, I use choice to define $F$ (for each $x$ I need to "choose" some appropriate $y$ to be $F(x)$, and if there are lots of $x$s and no easy way to describe appropriate $y$s, this is something I might need choice for). So the intuition should be that choice might be needed to show that the Skolem function exists.

And in fact this is correct, in the strongest possible way: the axiom of choice is Skolemization!

Clearly choice lets you Skolemize, so it's the other direction that's interesting. Suppose I have a family $\{A_i: i\in I\}$ of nonempty sets. The axiom of choice tells me that a choice function exists - that is, a map taking each $i\in I$ to some $a_i\in A_i$.

Now let's think about those two sentences:

  • Saying "each $A_i$ is nonempty" is just "For all $x$, there is some $y$ such that $y\in A_x$."

  • But saying "there is a choice function" is just "There is some $f$ such that for all $x$, $f(x)\in A_x$."

The axiom of choice goes from the nonemptiness statement to the function statement - and this is exactly Skolemization.

Noah Schweber
  • 245,398
  • You just switched $i$ for $x$, and that looks weirrrrrrddddddd... – Asaf Karagila Mar 07 '17 at 14:53
  • @AsafKaragila Yeah, I went back and forth on that, but I decided I wanted the variables to match up with the usual way Skolemization works. Besides, they're all bound variables anyways. :P – Noah Schweber Mar 07 '17 at 14:56
  • I accept your answer even though i can not vote :) . Your explanation is in plain text and help me a lot in understanding the axiom of choice . Thanks a lot. – Keith Mar 07 '17 at 15:24
  • @Keith You may not be able to vote, but accepting an answer is a separate action and I believe you can do that. – Fabio Somenzi Mar 07 '17 at 15:29
  • Interesting observation, +1 -- though perhaps a bit too slick: At the formal logic level, Skolemization gives you a new function letter, whereas the Axiom of Choice promises you a functional relation reified within set theory itself, so you can interpret it without extending the logical language. – hmakholm left over Monica Mar 07 '17 at 15:34
  • 1
    @HenningMakholm Sorry, by Skolemization I mean the new formula together with the semantic equivalence - the assertion that every first-order sentence $\varphi=\forall x\exists y\psi(x, y)$ is equivalent to the corresponding second-order sentence $\theta=\exists F\forall x\psi(x, F(x))$ (in the sense of having the same models) is in fact equivalent to the axiom of choice. – Noah Schweber Mar 07 '17 at 16:00
  • 1
    Ah, got it: it's AC at the metalevel. – hmakholm left over Monica Mar 07 '17 at 16:03
2

Fix a structure $M$ of your language, now you can think about every formula with a single free variable as defining a subset of $M$.

The statement that $\exists x\varphi(x)$ means that the set defined by $\varphi$ is non-empty.

But now a Skolem function is a function symbol $F$ such that when we interpret the extended language we get $M\models\exists x\varphi(x)$, then $M\models\varphi(F^M(x))$.

This means that in effect, $F$ is a choice function from all the definable subsets of $M$. But the axiom of choice is certainly needed here!

If $\{A_i\mid i\in I\}$ is any family of non-empty sets, taking the language with predicate symbols $R_i$ for $i\in I$ and the theory $\exists x R_i(x)$, then the structure $M$ whose universe is $\bigcup\{A_i\mid i\in I\}$ and $R_i^M=A_i$ satisfies the theory. And of course, a Skolem function is by definition a choice function from the $A_i$'s.

Asaf Karagila
  • 393,674