[FoM] Slater on epsilon terms and domains

[A.P. Hazen]

    Although I haven't been convinced by ALL of Hartley Slater's
philosophical claims for Hilbert's epsilon-calculus, I think his proposal
to understand rules like the constant-substitution quantifier rules in
Beth-Smullyan-Jeffrey tableau systems is very helpful.  The restrictions on
these rules, which can be confusing and mysterious and hard for beginning
students to remember(1), are very easy to understand if you think of the
instantial constants as ABBREVIATIONS for epsilon-terms: the restrictions
on the rules basically allow for unambiguous "disabbreviation".  The
fallacious "proofs" you can construct  if you ignore the restrictions
involve things like pairs of constants "abbreviating" epsilon-terms each of
which would have to be contained in the other!
    If, instead of abbreviating to a single symbol, you display the free
variables (and other subterms) occurring in epsilon-terms, they are in
effect Skolem functionals.  Therefore, the technical result Hartley refers
to-- the correctness and completeness of the epsilon-variant of tableau
systems-- has the following consequence for ordinary predicate logic:
    (*) If a First Order sentence is not formally refutable, then it
        is satisfiable in a model over what logic programmers call its
         "Herbrand Universe."
This is implicit in Gödel's original (1930) proof of the Completeness
Theorem, which makes use of Skolem Normal Forms.
---
(1)  Jeffrey's rule has the simplest, easiest to remember, restriction:
ALWAYS use a NEW constant when dealing with an existential quantifier.  As
a more interesting exercise, use the analysis of instantial terms as
"abbreviated" epsilon expressions to gain an intuitive understanding of the
more liberal restriction at the botom of page 54 of Smullyan's "First Order
Logic."  Or the restrictions on instantial constants in the natural
deduction system of Quine's "Methods of Logic".
---
References:
  For Hilbert's epsilon calculus: A. Leisenring, "Mathematical Logic and
Hilbert's [epsilon]-Symbol," London (MacDonald), 1960-something
  For longwinded, non-rigorous, discussion of instantial rules in natural
deduction and tableau systems as "abbreviated" epsilon-rules: A.P. Hazen's
article in "Journal of Philosophical Logic," v. 16 (1987).
---
Allen Hazen
Philosophy Department
University of Melbourne