[FOM] Skolem Functions

[A.P. Hazen]

Steve Stevenson asks:
>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?

Some possible ways in  which Skolem functions (and the terms 
expressing them) can seem evil:

(1) They need to be used VERY carefully once you go to intuitionistic 
or modal logics.  Suppose you cook up a proof-procedure incorporation 
the rule
      SKOLEMIZE: from a formula Ax1...AxnEy(...y...), starting with
           n universal and one existential quantifiers,
           infer
          	Ax1...Axn(...f(x1...xn)...),
             the formula obtained by dropping the existential
           quantifier and replacing occurrences of the
           variable by it with occurrences of the term
                 f(x1...xn)
           formed with a NEW function symbol and the variables
           bound to the universals.
This is a sound  system; one of the ideas in Quine's "Methods of 
Logic" is very similar to it.
      Introducing this rule in a formulation of intuitionistic logic, 
however, allows the derivation of intuitionistically invalid 
formulas, such as
      Ex(EyFy --> Fx).
Proof:  (1) Assume EyFy
         (2) Ff (fropm 1 by Skolemize)
         (3) (EyFy --> Ff) (conditionalizing, discharging assumption 1)
         (4) Ex(EyFy --> Fx) (from 3 by exist. quant. intro)
Use of Hilbert's "epsilon operator" or the Existential Instantiation 
rule of the  deductive system of "Methods of Logic" (editions 1,2, or 
4) has the same drawback from this point of view.
      As Tennant has already noted in a posting to FoM, Grigory Minc 
has discussed the extent to which  the epsilon-operator can be used 
in a formulation of intuitionistic logic: the relevant paper is in a 
collection of his papers published  by Bibliopolis.  A more semantic 
(=model theoretic) discussion by John Bell is in  "Journal of 
Philosophical Logic" v. 22 (1993), pp. 1-18.

      (2) IMPORTANT: Remember that this sort of rule can cause 
problems in modal (epistemic, etc) logics as well as intuitionistic. 
Berkeley's "Master Argument" for the inconceivability of unperceived 
matter arguably turns on a fallacy of this sort: cf. Graham Priest's 
formalization of Berkeley in his article in B.J. Copeland, ed., 
"Logic and Reality: essays on the legacy of Arthur Prior" 
(Oxford/Clarendon, 1996).  Other "paradoxes" may have similar....

      (3) Even in Classical contexts, Skolem function-symbols are 
**semantially** perhaps a bit puzzling.  To prove that the Skolem 
FUNCTIONS denoted by the symbols exist requires the Axiom of Choice. 
(Consider the example "Ax(x is a pair of socks  --> EyEz(y is one of 
the socks in x & z is one of the socks in x and Not-(x=y)))".)  Even 
if you use Skolem PREDICATES to reduce an arbitrary formula to Pi-2 
form (as Godel did in his completeness theorem paper, and as Church 
discusses in section 42 of the Bible) there is a semantic subtlety. 
In either Godel's or Church's algorithm, the new predicate 
representing an existential quantifier followed by universals will 
have as arguments all the variables bound by preceding UNIVERSAL 
quantifiers, AND all the variables bound by PRECEDING existential 
quantifiers, as well as the variable of the quantifier being treated. 
 From the point of view of getting a classically equi-satisfiable 
formula, you could simplify by using a predicate of lower degree: 
leave out the variables bound to earlier EXISTENTIAL 
qunatifiers------ BUT, in  that case, proving the existence of a 
relation to be the extension of the new predicate would require 
choice!  (The version using higher-degree predicates does not have 
this requirement.)
        One way of looking at Kit Fine's "arbitrary objects" system 
(Cf. his book, "Reasoning with Arbitrary Objects," though frankly I 
think most logicians don't have to go through  all the definitions 
in the book: Fine's shorter article in "Journal of Philosophical 
Logic" for 1985 (1984?) gives enough information about the technique) 
is that it is a way of constructing proof procedures with most of the 
advantages of Skolemization but without requiring Choice for the 
semantic interpretation of the formulas  used....

---

Allen Hazen
Philosophy Department
Univ of Melbourne