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-ZCNwHF9ErpZ2icitjWtXSw@xxxxxxxxxxxxxxxx> 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-+I05ep9qJbk3uPMLIKxrzw@xxxxxxxxxxxxxxxx
> http://www.cs.nyu.edu/mailman/listinfo/fom
--
Jesse Alama (alama-FGKo4X94FMn2fBVCVOL8/A@xxxxxxxxxxxxxxxx)
|
