FOM: Re: more on Hilbert, Monism and Optimism

[dubucs]

The present posting pursues the current exchange with Neil Tennant about
Hilbert's attitude towards decidability of mathematics. I can't manage to
make it intelligible without reproducing large parts of Tennant's last
posting.

Jacques Dubucs suggested (Jun 13 12:30:52 1999) that the following
considerations lend some credence to the claim that the early Hilbert
had global decidability in mind:
Look at the consistency proof sketched by Hilbert before the Heidelberg
congress (1904).
This consistency proof runs roughly as follows. Number theory is formalized
in such a way that
a) Every axiom has a certain morphological (decidable) property P
b) The property P is preserved by applying the inference rules of the system
c) The property P is not preserved by negation
Whence consistency immediately follows, for the negation of an axiom can't
be proved).  This consistency proof, if completely achieved,
would provide us with an effectively recognizable condition of provability
in number theory.

Neil Tennant answered (Jun 13 18:42 1999):
With respect, I disagree. If we take an arbitrary sentence S and
decide (effectively) whether it has the property P in question, and
happen to return a negative verdict, then this simply tells us that P
is not provable in the system in question. It does not suffice to show
that P is refutable---unless we know, on independent grounds, that the
system is theoretically complete. Then, but only then, would the
unprovability of S entail the refutability of S.

Here my answer (JD): I never said that Hilbert's sketched consistency
proof, if carried through, would have provided an effective algorithm of
*decision* for number theory. Of course no, for the property P is only a
*necessary* condition of provability, not a sufficient one. Nevertheless,
the possibility of effectively deciding between unprovability and
irrefutability, while obviously falling short of a full method of decision,
is a non-trivial step in this direction. Viewing that Hilbert found this
possibility very plausible in 1904, we are entitled to attribute him, even
in his early foundational writings, the kind of favouring attitude towards
the idea of mechanization of mathematics that I described in a former
posting (13 Jun 1999 18:42:34)

Incidentally, Johannes von Neumann, who was one of the most lucid members
of the Hilbertian School (and, anyway, the first to grasp the significance
of Goedel's incompletness results), found the kind of *morphological*
consistency proof that Hilbert attempted in 1904 very dubious, just because
its non-trivial implications concerning mechanizability (cf *Zur
hilbertschen Beweistheorie* (1927), in Collected Works, Pergamon Press,
1961, vol. 1, p. 276).

-----------------------
Tennant pursued (Jun 13 18:42 1999):
Is there any clue in Hilbert's early writings that he countenanced the
following possibility, with respect to a sentence S and a given theory?:

(1) the effective test (for the presence of property P) shows that S
    is not provable; and
(2) the effective test shows that not-S is not provable; while yet
(3) the logic underlying the theory is known to be complete
    (i.e. every logical consequence admits of finitary proof) ?

Here my answer (JD):
I suspect that there is no such possible clue, for a simple and well-known
reason. As lenthly and convincingly explained by Goedel in several places,
the very notions in terms of which your (3) is expressed were not available
to Hilbert, who was always very reluctant (and, by the way, unable) to
formulate the completness problems in such semantical terms. Moreover, one
can wonder if Hilbert's views favouring decidability were not a simple
by-product of his propensity of thinking the foundational problems in
exclusively syntactical terms (cf my posting of Jun 11 22:34:58 1999).

---------------------------
Tennant pursued (Jun 13 18:42 1999):
I agree with Dubucs that it is a highly non-trivial venture to specify
the epistemic constraints on a well-motivated axiomatic system, so as
to rule out the trivial addition of P as an axiom in order to "settle"
the conjecture P ('P' here is now a sentence, not a property), and in
order also to rule out other unmotivated additional axioms from which
P would trivially follow (...)
One possible way to constrain axiomatic extensions would be by
insisting that they take the form of reflection principles, starting
with some synthetic base theory and iterating on its reflective
extensions. But that would require arithmetization (coding of syntax)
or an equivalent device, which had not yet been thought of in 1917; so
it would a trifle anachronistic to suggest that Hilbert might have
been contemplating such a constraint.

Here my answer (JD):
I agree with Tennant that, if one accepts the idea that the ways of
not-trivially solving mathematical conjectures cannot be framed in one
single formal system, one is driven towards the idea of (a sequence of)
extensions of a "synthetic base theory". Of course, the rigourous idea of a
reflection principle was not at Hilbert's disposal in the tweenties to do
that.  But note that he proposes, in his latest *pre-goedelian* paper (*Die
Grundlegung der elementaren Zahlenlehre* (1931), Ges. Abh. III, 194),
another coarser way of dealing with the same kind of limits, namely by
introducing his omega-rule, that he warmly recommands as a "new FINITE
inference rule" ...

JD

Jacques Dubucs
IHPST CNRS Paris I
13, rue du Four
75006 Paris
Tel (33) 01 43 54 60 36
    (33) 01 43 54 94 60
Fax (33) 01 44 07 16 49