[FOM] Skolem functions

[Aatu Koskensilta]

On May 19, 2005, at 2:24 AM, Robert Black wrote:

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

There is a subtlety here. A function in constructive mathematics must 
be extensional, i.e. if A=B, where the =-relation depends on the 
underlying set, then f(A)=f(B). There is no requirement that the f 
furnished by the proof of AxEyFxy is extensional.

This is precisely the reason why the axiom of choice is in general not 
constructively valid, and in fact (with extensionality) implies the law 
of the excluded middle.

But this certainly is not my area of expertise, so I might be wide off 
the mark. Caveat emptor.

Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus