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

*To*: fom@math.psu.edu*Subject*: FOM: role of formalization in f.o.m.*From*: Stephen G Simpson <simpson@math.psu.edu>*Date*: Thu, 3 Jun 1999 20:34:28 -0400 (EDT)*In-Reply-To*: <199906010731_MC2-77C2-B5F8@compuserve.com>*Organization*: Department of Mathematics, Pennsylvania State University*References*: <199906010731_MC2-77C2-B5F8@compuserve.com>*Reply-To*: simpson@math.psu.edu*Sender*: owner-fom@math.psu.edu

In response to Robert Tragesser's questions of 1 Jun 1999 07:31:05, let me indicate why I think formalization is of the essence in foundational research, including f.o.m. I will *not* attempt to be ``unprecedentedly careful'' (cf. Friedman 31 May 1999 17:15:47). All I want to do is convey a certain idea or outlook that I think is common currency among f.o.m. researchers. When I teach introductory courses in mathematical logic and f.o.m., I always try (and sometimes even succeed!) to convey this outlook to the students. Recently I tried to convey something of this same outlook in an article intended for a general audience. The article will appear as a chapter of a volume called ``The Treasury of Philosophy'', to be published by the Book-of-the-Month Club. Here goes. When a scientific discipline or field of study reaches a certain degree of maturity, it is desirable to reify or codify the existing knowledge in terms of basic concepts and principles. An example is Euclid's reification of geometry in the Elements, in terms of ``common notions'', ``axioms'', ``postulates'', ``definitions'', ``theorems'', ``propositions'', ``lemmas'', etc. [ Digression: The kind of reification of subjects that I have in mind is *perhaps* the same as what Tragesser describes as ``the process of uncovering and articulating and recasting a subject matter according to its first or essential or most central principles''. Tragesser and maybe other philosophers refer to this as ``formalization''. I reserve the term ``formalization'' for a particular, precise version of this, based on the predicate calculus. See below. Tragesser says: > But of course this process was first discovered by Plato (on at > least Bill Tait's reading of Plato or moy reading of Bill Tait's > reading). Could Tragesser please give a reference for his idea that this notion of ``formalization'' (Tragesser's term) goes back to Plato? I think of it as going back to Aristotle. But then again, I am not a philosopher or a historian of philosophy. End of digression. ] If we set out to perform and study the reification of subjects in a highly systematic manner, we are led to questions such as: Which concepts and propositions are to be taken as basic for a given subject? How are the non-basic concepts and propositions to be derived from the basic ones? How can we be sure that nothing has been omitted? The predicate calculus has emerged as a precise language in which to study these and similar questions. In particular, we can use the strictly formal discipline imposed by the predicate calculus in order to say with certainty and precision that no basic concepts or assumptions have been omitted. >From this point of view, a completely worked out reification of a subject is nothing but a formal theory T in the predicate calculus. The basic concepts are then known as the primitives of T, and the basic propositions are known as the axioms of T. The process of working out a formal reification of a subject, usually in the predicate calculus or some inessential variant of it, is what I and other f.o.m. researchers call *formalization*. Some of the considerations which dictate the use of the predicate calculus here, rather than some other formalism, are: (i) The predicate calculus as a language is sufficiently rich and flexible to express every scientific proposition, but not so rich as to be able to express a lot of obviously flaky or non-scientific propositions. (ii) The predicate calculus is topic-neutral, in the sense that it has no subject matter or scientific assumptions of its own, so it forces us to explicitly introduce all of the basic concepts that are needed for the given subject matter as primitive predicates of T. Other concepts are then introduced as additional predicates in terms of definitional extensions. (iii) The predicate calculus provides a precisely defined, correct, adequate notion of logical consequence. The G"odel completeness theorem shows convincingly that, for propositions A and B in the predicate calculus, A implies B formally if and only if B follows from A *necessarily*, i.e., regardless of the meanings of the predicates that are involved, i.e., in all conceivable structures of the appropriate type. (iv) Using this, we have a way to be sure that a given set of axioms is adequate, by verifying that all the known propositions of the given subject are logical consequences of the axioms. The above scheme of formalized reification of subjects in the predicate calculus is obviously a scientifically desirable goal. However, to date it has been convincingly carried out only in a few cases, mostly limited to mathematics. Outstanding examples: first-order arithmetic, Tarski's elementary geometry, second-order arithmetic (i.e. arithmetic plus geometry), ZFC. Thus the study of these and related formal theories in the predicate calculus and the formalization of mathematics within them is an essential part of modern f.o.m. research. My reading of the history of the contemporary 20th century concept of ``mathematical rigor'' is that it evolved, on a parallel track, from the same sorts of considerations that also gave rise to the above idea of formalization within the predicate calculus. This is part of why it is usually or at least often a fairly straightforward exercise to formalize detailed rigorous mathematical expositions in the predicate calculus. In principle, none of this has anything in particular to do with mathematics. In principle, the above general scheme (formalized reification in the predicate calculus) is applicable to any scientific subject whatsoever. But to date it has been worked out only in mathematics. In this sense, f.o.m. serves as a model or example of what can be hoped for in the future in the way of rigorous or formal foundations of other scientific subjects. I hope this explanation addresses some of Tragesser's concerns. -- Steve

**Follow-Ups**:**Robert Black**- Re: FOM: role of formalization in f.o.m.

**References**:**Robert Tragesser**- RE: FOM: formalization

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

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