[FOM] Skolem functions

[Jesper Carlstrom]

This problem has been debated a lot. The reason for it being a problem is
that there are several versions of the axiom of choice around, some are
constructive, some are not. For some explanations and references you can
have a look at my short note: http://dx.doi.org/10.1002/malq.200410100.

Best regards,
Jesper Carlstrom

Jesse Alama wrote:
> Consider the formulas (in OTTER syntax)
>
> A: all x exist y p(x,y)
> B: all x p(x,f(x)).
>
> Clearly, if B is valid then A is valid.  If A is valid, then, by the
> axiom
> of choice, B is valid.  Thus the equivalence of the validity of A and B
> depends on a nonconstructive principle, namely the axiom of choice.
> Perhaps this explains why, in the rules for intuitionistic tableaux,
> skolemization is forbidden.