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

*To*: fom@math.psu.edu*Subject*: FOM: this and that*From*: holmes@catseye.idbsu.edu*Date*: Tue, 28 Dec 1999 17:13:54 -0700*Sender*: owner-fom@math.psu.edu

Happy Holidays to everyone, and enjoy the Millennium Bug (and next year the Millennium :-) Re the proper definition of mathematics: Mathematics is the study of abstract data types, specifiable in the language of second-order logic (there is no requirement here that the mathematician actually specify them this way :-), without qualms about the possibility of implementation (the last clause indicates why mathematics is not subsumed by theoretical computer science). Re things which ought to happen in the future in FOM (I'm not going to say what _will_ happen): I hope that the hypnotic influence of the truly marvellous and useful theorems about first-order logic lifts enough for more mathematicians to recognize that second-order logic is also ... logic. First-order logic is vitally important as the basic machine of inference, but second-order logic is needed for the (equally "logical") purpose of enabling the precise definition of mathematical concepts. It is of course inconvenient that second-order logic does not admit complete rules of inference (but it inherits perfectly adequate partial rules of inference from first-order logic, with rules for quantification extended to second-order quantifiers). Higher order logics are interpretable as second-order logic with extra non-logical assumptions. I hope that philosophy of mathematics and general philosophy begin talking to each other, particularly about "ontological commitments". The effect of this will probably be to cast some doubt on the wisdom of relying on a system as strong as ZFC (or even as strong as the theory of types or NFU with infinity), since these systems talk about very large worlds! I certainly hope that the former beautiful systems (and even stronger ones) continue to be studied (I decline to be driven out of Cantor's paradise :-), but I would guess that the right level of strength for a foundational system is somewhere around the level of third order arithmetic (the strength of the second-order theory of real numbers). Of course, if one thinks that the world is finite or that the world is infinite but discrete then one might prefer still weaker systems. (Nothing here is intended to discourage investigations of assertions about small structures which have high consistency strength; in fact the viewpoint suggested here should encourage such investigations as demonstrating the applicability of strong systems whose ontological commitments are dubious.) I hope that truly user-friendly systems for computer-assisted reasoning come into general use; I think that we are just short of the threshold for such systems to be of practical use to at least some mathematicians (I would not suggest my own theorem prover for this purpose; I'm thinking of something like an extension of Mizar). Certainly the demands of theoretical computer science will continue to act strongly on the foundations of mathematics (for one thing, computer scientists are often more conscious of their foundational needs than mathematicians: witness my borrowing of the term "abstract data type" for the purposes of a definition of mathematics above), so we ought to get something in return! And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes the gates of Cantor's paradise, that the | Boise State U. (disavows all) slow-witted and the deliberately obtuse might | holmes@math.boisestate.edu not glimpse the wonders therein. | http://math.boisestate.edu/~holmes

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

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