[FOM] Skolem functions

[Jesse Alama]

Hi Robert,

Consider the gentzen system G1i of [1] for intuitionistic first-order
logic.  (I take it for granted that G1i's proofs are "constructive".
My identification of "intuitionism" and "constructivism" certainly
deserves comment and I would appreciate any references that would show
the connection between these two ideas.)  If for a formula P we have
that G1i proves AxEyP, then in the deduction D that witness the
provability judgment the last step is an application of the right
universal rule, and the penultimate step is an application of the
right existential rule; above this we have a deduction D' of an
instance of P.  This analysis suggests the following synthesis: put

  P := Q -> Q

where Q is a propositional variable, and consider the deduction

        Q => Q
  ---------------
  =>    Q -> Q
  ---------------
  =>  Ey(Q -> Q)
  ---------------
  => AxEy(Q -> Q)

No functions were introduced in this deduction.  Thus, I'm not sure
what Dummett could have meant, for it seems that my deduction is a
counterexample to his claim.  Perhaps I simply misunderstand the
claim.  Could you please elaborate?

Warm regards,



Jesse

[1] A. S. Troelstra and H Schwichtenberg: _Basic Proof Theory_ (2nd
edition).

Robert Black <Mongre at gmx.de> writes:

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

-- 
Jesse Alama (alama at stanford.edu)