[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry*From*: Stephen G Simpson <simpson@math.psu.edu>*Date*: Fri, 4 Jun 1999 15:19:40 -0400 (EDT)*In-Reply-To*: <l03130301b37d64e15aea@[128.243.201.124]>*Organization*: Department of Mathematics, Pennsylvania State University*References*: <199906010731_MC2-77C2-B5F8@compuserve.com><l03130301b37d64e15aea@[128.243.201.124]>*Reply-To*: simpson@math.psu.edu*Sender*: owner-fom@math.psu.edu

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

**References**:**Robert Tragesser**- RE: FOM: formalization**Robert Black**- Re: FOM: role of formalization in f.o.m.

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]