[FOM] Skolem functions

[Robert Black]

No, that can't be right. A constructive proof of AxEyFxy consists 
precisely in the presentation of a function f such that AxFxf(x), so 
Choice in the form AxEyFxy->EfAyFxf(x) is intuitionistically valid 
(see for example Michael Dummet's book)..

>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.
>
>Jesse