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

*To*: fom@math.psu.edu*Subject*: FOM: Tragesser; full formalization; Lakatos; reverse mathematics*From*: Stephen G Simpson <simpson@math.psu.edu>*Date*: Mon, 7 Jun 1999 15:07:55 -0400 (EDT)*Organization*: Department of Mathematics, Pennsylvania State University*Reply-To*: simpson@math.psu.edu*Sender*: owner-fom@math.psu.edu

Robert Tragesser 4 Jun 1999 21:53:19 > Simpson tries to evade the problem -- Tragesser is wrong to accuse me of evasion simply because I may not agree with him or may not care about allegedly important issues that seem to excite him. Robert, please try to concentrate on scientific issues and avoid psychological analysis. > implicitly raised by the apparently further seeing Friedman -- Tragesser seems to think that Friedman partially agrees with him, but I am not so sure. I will let Friedman speak for himself. > by making "involving a logical calculus" analytic of "full > formalization". Tragesser seems to want to say that full formalization does not necessarily involve a logical calculus. I confess I have no idea what Tragesser is talking about, because I have never considered the idea that a piece of mathematics can be fully formalized without using a logical calculus. This idea seems absurd to me. In my posting of 31 May 1999 19:36:19, I distinguished among three or four different senses of ``formalization''. These distinctions may be relevant to Tragesser's complaints and demands. Could Tragesser please try to explain his point? In particular, could Tragesser please indicate an example of what he considers full formalization that doesn't involve a logical calculus? Tragesser: > Here again is what must be done to make fom research fundamental > science -- This is obviously incorrect. F.o.m. is already fundamental science, without having done this. > to begin with a natural hbistory of mathematical proof , describing > carefully the operations, somewhat "dialectical" in character -- > that legitimately lead from informal proof to its "formalization", > remarking at each point of what has changed, what has been left > behind, an full evaluzation of what has been left behind, the > legitimacy of those changes, the sense in which the changes do and > do not preserve identity of proof. This style of analysis of mathematical proof may or may not be interesting and worthwhile. I think Lakatos attempted this in ``Proofs and Refutations'' for the V-E+F=2 theorem. ``Proofs and Refutations'' certainly created a splash among academic philosophers, but I don't think it had much impact on f.o.m. research. A good critique of Lakatos is in Feferman's essay ``The Logic of Mathematical Discovery versus The Logical Structure of Mathematics''. In particular, Feferman illustrates how the logical techniques that are normally used in f.o.m. research can account for the same kinds of phenomena as the Lakatosian dialectic, but in a more rigorous way. In particular, there is reverse mathematics, as in part A of my book ``Subsystems of Second Order Arithmetic'' <http://www.math.psu.edu/simpson/sosoa/>. It is true that reverse mathematics primarily analyzes provability in specific formal systems, not the structure of particular proofs. However, reverse mathematics does sometimes manage to distinguish between two different proofs p1 and p2 of the same theorem t, by showing that the axioms needed to prove t are not as strong as the axioms needed to prove a particular lemma l occuring in some known proof of t. As an example, let t = ``every countable commutative ring has a prime ideal'' l = ``every countable commutative ring has a maximal ideal'' p1 = the usual textbook proof of t, via l p2 = a more complicated proof of t, formalizable in WKL0 It is known from reverse mathematics that t,l are equivalent to WKL0, ACA0 respectively, over RCA0. Thus the two proofs p1 and p2 of t are certainly not equivalent to each other. This kind of analysis of proofs has obvious advantages over the Lakatosian dialectic, because it is more mathematically rigorous. -- Steve

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

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