3 ms·

This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human wh

This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is a new idea that (some) computer programmers want to impose on the field (for the understandable reason that it makes computers primary). Formal proof only emerged early in the 20th century, and the standard became that in theory a proof should be formalizable to answer any skepticism, but the real goal in Euclid's time and ours has been to communicate why a theorem is true to your fellow humans. There were a few theorems that are only known via computer proof, like the Four Color Theorem, but this has always been regarded as disappointing or even controversial, and the fact that there hasn't been any conceptual breakthrough has meant that we didn't learn anything other than the sheer fact that the Four Color Theorem is true. Theorems that produce understanding, on the other hand, typically produce many new ideas that lead to more theorems. The purpose of scholarship is understanding. This is just as true for science as it is for math. If AI produces a unified theory of fundamental physics, but it's just an opaque blob, physicists will find it just as unsatisfying.

pcfwik 19d ago
I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing. However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong: > Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...] You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.) What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic. Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.
- QuesnayJr 17d ago
  The idea that logic is a branch of mathematics is itself a modern notion. Aristotle's logic was part of the trivium (grammar, rhetoric, and logic) in classical notions of education, while mathematics made up several parts of the quadrivium (arithmetic, geometry, music, and astronomy). Of course in retrospect we can see that the syllogistic part of Aristotle's logic can be formalized (as can grammar), but it was viewed as part of language or philosophy. I get the impression that a lot of more traditional philosophers of logic hated the formal turn. Leibniz anticipated the turn towards formalism, but he didn't publish any of it in his life and it wasn't rediscovered until the 20th century.
  - pcfwik 14d ago
    Agreed that logic isn't a branch of mathematics (even today, my experience has been that logic classes tend to be offered by philosophy departments, not math). My only quibble was the implication that logic is somehow much newer than mathematics (/Euclid). It's not like people suddenly woke up one day in the 20th century and thought for the first time: "huh, I wonder what separates correct arguments from incorrect ones?" But point taken that Aristotle was not as formalist in his time. If you have some sources to read more about this: > I get the impression that a lot of more traditional philosophers of logic hated the formal turn. I would be very interested! (Don't doubt it at all, just sounds like an interesting period I don't know as much about as I'd like.)

pcfwik 19d ago

I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing. However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong: > Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...] You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.) What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic. Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.

QuesnayJr 17d ago
The idea that logic is a branch of mathematics is itself a modern notion. Aristotle's logic was part of the trivium (grammar, rhetoric, and logic) in classical notions of education, while mathematics made up several parts of the quadrivium (arithmetic, geometry, music, and astronomy). Of course in retrospect we can see that the syllogistic part of Aristotle's logic can be formalized (as can grammar), but it was viewed as part of language or philosophy. I get the impression that a lot of more traditional philosophers of logic hated the formal turn. Leibniz anticipated the turn towards formalism, but he didn't publish any of it in his life and it wasn't rediscovered until the 20th century.
- pcfwik 14d ago
  Agreed that logic isn't a branch of mathematics (even today, my experience has been that logic classes tend to be offered by philosophy departments, not math). My only quibble was the implication that logic is somehow much newer than mathematics (/Euclid). It's not like people suddenly woke up one day in the 20th century and thought for the first time: "huh, I wonder what separates correct arguments from incorrect ones?" But point taken that Aristotle was not as formalist in his time. If you have some sources to read more about this: > I get the impression that a lot of more traditional philosophers of logic hated the formal turn. I would be very interested! (Don't doubt it at all, just sounds like an interesting period I don't know as much about as I'd like.)