FOM: Re: RE: FOM Arbitrary Objects
wwwtx at midway.uchicago.edu
Tue Feb 5 14:33:15 EST 2002
On Tuesday, February 5, 2002, at 06:27 AM, charles silver wrote:
for the epsilon-intantiation to
work, some particular element must always be plucked out of the range of
objects over which ExFx ranges. That is, an element having F must be
somehow obtained ("chosen") from all the F's.
Hilbert regarded the epsilon terms as denoting `ideal objects'; and his
hope (probably one should say: conviction) was that in any formal
deduction of a variable-free formula, they could be eliminated. But if
one were to give a `semantics' for the epsilon-calculus, it would not
be necessary to interpret epsilon x F(x) as denoting an F---for example,
if there are no F's, it could denote anything. Likewise, in eliminating
this epsilon term in a deduction, if there are no critical formulas F(t)
arrow F(epsilon x F(x) in the deduction, then epsilon x F(x) can be
replaced by any term.
On the other hand, Charles was responding to Jay Halcomb who wrote
Hilbert used the epsilon symbol to elucidate the notion of an arbitrary
selection, which he axiomatized in the epsilon-calculus.
This is surely wrong, too: Hilbert introduced the epsilon terms as a
tool in his proof theory. I do believe that the notion of an arbitrary
number has a place in his philosophy---in understanding his finitism;
but I see no place for it in his conception of the epsilon-calculus.
> Of course, one has to admit that some of its
> popularity is that it's attached to a famous person. If Joe Blow had
> invented it, we'd have no "Blow's epsilon calculus" at all.
Is Joe Blow an arbitrary person? If so, perhaps we _should_ pay more
attention to Hilbert. But, if we do, then it won't lead us down the path
being discussed by Charles and Jay.
Incidentally, for a very nice discussion of the history of the
epsilon-calculus and substitution method, see Jeremy Avigad and Richard
Jeremy posted a notice about this yesterday---perhaps as a hint.
More information about the FOM