Hmmmm, > > All mathematicians agree that a mathematical proof is something that > could eventually be written as an axiomatic proof using the accepted > set theory axioms (ZFC: the Zermelo-Frankel axioms plus the axiom of > choice). These axiomatic proofs could then be checked for correctness > by a computer program.
Is this really true? No doubt, an axiomatic proof is a pretty convincing mathematical model of proof. (Oh, and such things can be checked by computer program, yep.) But, is it the case that every thing which constitutes a proof could be expressed as a ZFC-axiomatic proof instead? (I suppose that if all mathematicians really agreed on this point, then this would be true on the "accepted by the community" notion of proof. But that's probably not what was meant by the claim. [and perhaps I found the joke too tempting....]). I've got two levels of concern: 1) at the connection between pure and applied mathematics. Does everything which convinces (mathematically) in practice have a reduction (or should that be expansion) to some formal system of proof? 2) just within pure math: Can every object which is a valid formal proof be converted to a ZFC proof? Just to be clear, I think proof is still a useful thing. Something we should probably teach to kids more often. And a nice ZFC proof does give me a warm glow. But the quoted claim just struck me as too strong. Maybe, I've been a distant spectator for too long...and I've forgotten some important stuff. mew ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
