3 ms·
Isn't this just a rehash of the lates 19th/early 20th century intuitionits vs. formalists debate? Even though Gödel had shown that the ultimate goal of the form
by fhars 18y ago
Isn't this just a rehash of the lates 19th/early 20th century intuitionits vs. formalists debate? Even though Gödel had shown that the ultimate goal of the formalist program is unattainable, they still mostly won that debate by being able to produce more meaningful results. The radical intuitionist, with whom the author seems to sympathize, did not only reject the axiom of choice, but even things like the law of the excluded middle (i.E. they assumed that "A or not A" is not necessarily true). That makes many proofs considerably harder to perform, if not totally impossible.
Not surprisingly, the formalist program was also more fruitful for endeavours like computational logic and the theory of computation, which resonate with the formalist tenet that mathematics is just the manipulation of strings of abstract symbols according to specific rules.
This http://en.wikipedia.org/wiki/Brouwer-Hilbert_controversy http://en.wikipedia.org/wiki/Brouwer-Hilbert_controversy gives some of the context.
- ionfish 18y agoI can't remember where I originally found this link (I thought it was here, but a quick check of SearchYC didn't reveal it), but I found the following article on intuitionistic mathematics for physics pretty fascinating. While I know a certain amount about intuitionistic mathematics, I'd never really considered that people might actually use it. http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/ http://math.andrej.com/2008/08/13/intuitionistic-mathematics...
- harshavr 18y agoI dont think the debate was as much between intuitionism and formalism as it was between intuitionists and people who thought infinite objects are really real. In particular, intuitionists dont object to "A or not A" for finite sets. In many cases theories become simpler not more complicated with constructive foundations for mathematics, (for instance, synthetic differential geometry is a much more elegant way of doing geometry). Modern categorical foundations for mathematics, using topos theory, has intuitionistic logic as its natural language. It is exactly constructive foundations of mathematics which is related to foundations of programming languages, and this in many cases is formalized via the Curry-Howard correspondence which takes programs to proofs and vice versa.
- yummyfajitas 18y agoI think it's more a "Humans vs Computers" debate. Some background: Tom Hales cleverly reduced the Kepler Conjecture to the solution thousands of linear programming problems: if all the solutions are bigger than something, the kepler conjecture is true. Then he had a computer solve the LP problems, and the result was that Kepler was true. However, his solution was informal in the following sense; he didn't have a rigorous proof that the solution of the LP problems was accurate, nor were his programs proven correct. Now he is attempting to redo the proof in HOL, a formal theorem proving system. More background: no math paper is completely formal. All involve some handwaving, especially the 200 page monsters that appear in Annals of Math. An example from a paper I'm currently writing: "It can be easily seen by elementary calculus arguments that..." Doron is arguing that the mathematical community is holding Hale's computer proof to a higher standard than it would hold a comparable 200 page human-written paper. Basically, he is claiming that we should accept an informal computer-assisted proof just like we would accept an informal human-written proof.