FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry

[Stephen G Simpson]

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