[FOM] Skolem functions

[Jesse Alama]

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

Steve Stevenson <steve at cs.clemson.edu> writes:

> When I took a course in automatic theorem proving many years ago, the 
> instructor railed against Skolem functions for reason I have never 
> understood. Now, while doing some work with intuitionistic tableaux, 
> I find comments that Skolem functions are not allowable. Would 
> someone explain this to me. Is this because they're magic functions 
> of some sort?
> -- 
> best,
> steve
>
> Dr. D. E. Stevenson
> Director, Institute for Modeling and Simulation Applications
> Clemson University
> Clemson,SC 29634-0974
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-- 
Jesse Alama (alama at stanford.edu)