FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry
Stephen G Simpson
simpson at math.psu.edu
Fri Jun 4 15:19:40 EDT 1999
Robert Black 4 Jun 1999 12:17:59
> There is much to agree with in Steve's account of what is involved
> in formalization,
Good, I am glad you found much to agree with.
> and (as Steve is probably well aware) much of what he says bears a
> striking resemblance to Hilbert's well-known 1917 lecture
> 'Axiomatisches Denken'.
No, I wasn't aware of Hilbert's remarks. Thanks for that reference.
I infer that great minds think alike! :-) (Just kidding.)
Seriously, I may have read Axiomatisches Denken at some time in the
past. I don't think so, but it is possible. In any case, as I said
in my posting of 3 Jun 1999 20:34:28, these ideas are common currency
among f.o.m. researchers. I never claimed any originality.
Black:
> The striking difference between Steve and Hilbert, however, is
> Steve's insistence that the tool of formalization be first-order
> logic.
A few points about this.
1. I want to call it predicate calculus, rather than first-order
logic. The reason for calling it predicate calculus is that I now
think calling it first-order logic invites confusion and ambiguity
regarding so-called second-order and higher-order logic, of the
kind promulgated in Shapiro's book. See also my many FOM postings
of February 1999 and March 1999 entitled ``second-order logic is a
myth''.
2. Actually, in 3 Jun 1999 20:34:28 I hedged a little bit and asked
for something like ``the predicate calculus or an inessential
variant thereof''. I am open to discussion about this. In judging
whether a given formalism meets my standards, I would want to know
that it has strictly formal, syntactical rules of inference and an
appropriate completeness theorem, similar to G"odel's completeness
theorem for the predicate calculus. Systems based on untyped
lambda calculus would probably qualify. Systems based on typed
lambda calculus or type theory might also qualify, so long as we
are talking about something like what Shapiro calls ``Henkin
semantics''. Shapiro's so-called ``second-order logic with
standard semantics'' would certainly not qualify.
3. My insistence on the predicate calculus may or may not make a
difference vis a vis Tragesser's original demand in 1 Jun 1999
07:31:05. Tragesser wants f.o.m. professionals to give him an
``unprecedentedly careful'' demonstration of the necessity or
appropriateness of formalization. But what Tragesser means by
``formalization'' is not at all clear (keep in mind his references
to Tait and Plato), so Hilbert's idea of a logical calculus may be
just as relevant vis a vis Tragesser's demand as the predicate
calculus. For that matter, any kind of rigorous mathematics, even
at the level of Euclid's Elements, may also be just as relevant vis
a vis Tragesser's demand. It's hard to know for sure, because
Tragesser hasn't drawn the appropriate distinctions, at least not
here on the FOM list.
Black:
> Hilbert wanted formalizations such that the axioms 'alone suffice
> to build up the whole framework from logical principles' and for
> Steve a requirement of formalization is that 'nothing has been
> omitted' and 'all the known propositions of the given subject are
> logical consequences of the axioms'.
Yes. The Hilbert/Simpson attitude about this is that, if you find
that there are known propositions of the given subject that are not
logical consequences of the axioms you have laid down, then this is in
some sense a pretty good indication that additional axioms are needed.
Don't you agree?
> But surely the greatest result of twentieth-century f.o.m. research
> is that in general this *can't be done*.
To say ``in general this can't be done'' is too crude. There are
significant senses in which this *can* be done. For example, it is
correct and important to understand that the axioms of ZFC are
adequate to derive the bulk of modern mathematics. It is correct and
important to understand that the axioms of PA are adequate for
arithmetic. Et cetera, et cetera. (See also the early discussion of
``practical completeness'' here on the FOM list.)
> Goedel didn't stop with his completeness theorem!
Of course I haven't forgotten about the G"odel incompleteness theorem,
and I am well aware that the problem of how to cope with the
incompleteness phenomenon is a major issue or complex of issues in
contemporary f.o.m. research. Nevertheless, I claim that the
incompleteness phenomenon does not invalidate my comments in 3 Jun
1999 20:34:28 on the role of formalization. (They may invalidate
Hilbert's comments in Axiomatisches Denken, if Hilbert insisted that
the axioms be complete in the familiar sense, i.e. all sentences are
provable or refutable.)
> Incidentally, in just what sense is second-order arithmetic (as a
> two-sorted first-order theory, of course) 'arithmetic plus
> geometry'?
Ah, good, I was hoping that somebody would pick up on this.
The idea is to view second-order arithmetic as an amalgam of
elementary arithmetic and elementary geometry. I have been playing
with this as a way of explaining or motivating second-order arithmetic
as a natural framework for f.o.m. studies of a certain kind.
A formal result that backs this up:
Let GZ be Tarski's elementary geometry augmented by a 1-ary predicate
Z for the integers, with the completeness axioms extended to formulas
involving Z, plus additional axioms saying that the integers are
evenly spaced points along a line. Then GZ is biinterpretable with
second-order arithmetic in a nice way.
(I haven't checked the proof of this, but it seems OK. Does anybody
know a reference for this kind of thing?)
-- Steve
More information about the FOM
mailing list