3 ms·

The part about proofs and axioms is completely non-logical. for the past several centuries, proofs have relied on axioms. Euclid introduced axioms (postulates)

by Drbble 15y ago

The part about proofs and axioms is completely non-logical. for the past several centuries, proofs have relied on axioms. Euclid introduced axioms (postulates) in order to provide proofs (and precise formulations) for informal statements. So the math part is really more an argument in favor of classes as a sort of axiomitization of computing.

pavpanchekha 15y ago
The majority of the proofs Euclid produced existed, both as theorem and proof, before his time. Similarly, few recent mathematical advances have started with formalizations and axioms. Calculus wasn't put on a rigorous basis until Lebesgue's time, hundreds of years after Newton and Leibniz. Category theory needed quite some work before it was formalizable. Differential geometry wasn't that rigorous until the twenties or so. Complex analysis was developed using many, many unnecessary assumptions because the formalities weren't there. I'm not picking-and-choosing math fields here; these are just the ones I'm familiar ones. It turns out, axiomatization and theory-building are two separate jobs rarely performed by the same mathematician. Usually, the theory-building makes the mathematician famous, and the axiomatization does not, but this is in many ways a tragedy. In any case, to the outsider of mathematics, it seems that axioms come first. This is false -- axioms come much later, because the work of axiomatizing isn't worth it before the theory proves itself useful. Axioms come first in a formal way, in the same way classes come first in a formal way. But the interesting thing isn't the class -- it's the instance. And in the same way, the axioms aren't interesting -- it's the resulting theories. I found the analogy very insightful.
empthought 15y ago
Lakatos's [Proofs and Refutations](http://www.worldcat.org/oclc/258084194 http://www.worldcat.org/oclc/258084194) is good background on the mathematical ideas that Stepanov is alluding to. The short version is that you don't start with axioms, because they are generally uninteresting. You start with interesting theorems and if necessary revise the set of axioms needed to prove those theorems.

by Drbble 15y ago

pavpanchekha 15y ago

The majority of the proofs Euclid produced existed, both as theorem and proof, before his time. Similarly, few recent mathematical advances have started with formalizations and axioms. Calculus wasn't put on a rigorous basis until Lebesgue's time, hundreds of years after Newton and Leibniz. Category theory needed quite some work before it was formalizable. Differential geometry wasn't that rigorous until the twenties or so. Complex analysis was developed using many, many unnecessary assumptions because the formalities weren't there. I'm not picking-and-choosing math fields here; these are just the ones I'm familiar ones. It turns out, axiomatization and theory-building are two separate jobs rarely performed by the same mathematician. Usually, the theory-building makes the mathematician famous, and the axiomatization does not, but this is in many ways a tragedy. In any case, to the outsider of mathematics, it seems that axioms come first. This is false -- axioms come much later, because the work of axiomatizing isn't worth it before the theory proves itself useful. Axioms come first in a formal way, in the same way classes come first in a formal way. But the interesting thing isn't the class -- it's the instance. And in the same way, the axioms aren't interesting -- it's the resulting theories. I found the analogy very insightful.

empthought 15y ago

Lakatos's [Proofs and Refutations](http://www.worldcat.org/oclc/258084194 http://www.worldcat.org/oclc/258084194) is good background on the mathematical ideas that Stepanov is alluding to. The short version is that you don't start with axioms, because they are generally uninteresting. You start with interesting theorems and if necessary revise the set of axioms needed to prove those theorems.