“An algebraic proof is a series of steps that you can tell are locally licensed because they maintain balanced weights”, but it seems like an obvious direct specialization of “syntactic implication should preserve semantic implication”
Eliezer, I very much like your answer to the question of what makes a given proof valid, but I think your explanation of what proofs are is severely lacking. To quote Andrej Bauer in his answer to the question “Is rigour just a ritual that most mathematicians wish to get rid of if they could?”, treating proofs as syntatic objects “puts logic where analysis used to be when mathematicians thought of functions as symbolic expressions, probably sometime before the 19th century.” If the only important thing about the steps of a proof are that they preserve balanced weights (or semantic implication), then it shouldn’t be important which steps you take, only that you take valid steps. Consequently, it should be either nonsensical or irrelevant to ask if two proofs are the same; the only important property of a proof, mathematically, validity (under this view). But this isn’t the case. People care about whether or not proofs are new and original, and which methods they use, and whether or not they help give a person intuition. Furthermore, it is common to prove a theorem, and refer to a constant constructed in that proof. (If the only important property of a proof were validity, this should be an inadmissible practice.) Finally, as we have only recently discovered, it is fruitful to interpret proofs of equality as paths in topological spaces! If a proof is just a series of steps which preserve semantic implication, we should be wary of models which only permit continuous preservation of semantic implication, but this interpretation is precisely the one which leads to homotopy type theory.
So while I like your answer to the question “What exactly is the difference between a valid proof and an invalid one?”, I think proof-relevant mathematics has a much better answer to the question you claimed to answer “What exactly is a proof?”
(By the way, I highly reccomend Andrej Bauer’s answer to anyone interested in eloquent prose about why proof-relevant mathematics and homotopy type theory are interesting.)
Eliezer, I very much like your answer to the question of what makes a given proof valid, but I think your explanation of what proofs are is severely lacking. To quote Andrej Bauer in his answer to the question “Is rigour just a ritual that most mathematicians wish to get rid of if they could?”, treating proofs as syntatic objects “puts logic where analysis used to be when mathematicians thought of functions as symbolic expressions, probably sometime before the 19th century.” If the only important thing about the steps of a proof are that they preserve balanced weights (or semantic implication), then it shouldn’t be important which steps you take, only that you take valid steps. Consequently, it should be either nonsensical or irrelevant to ask if two proofs are the same; the only important property of a proof, mathematically, validity (under this view). But this isn’t the case. People care about whether or not proofs are new and original, and which methods they use, and whether or not they help give a person intuition. Furthermore, it is common to prove a theorem, and refer to a constant constructed in that proof. (If the only important property of a proof were validity, this should be an inadmissible practice.) Finally, as we have only recently discovered, it is fruitful to interpret proofs of equality as paths in topological spaces! If a proof is just a series of steps which preserve semantic implication, we should be wary of models which only permit continuous preservation of semantic implication, but this interpretation is precisely the one which leads to homotopy type theory.
So while I like your answer to the question “What exactly is the difference between a valid proof and an invalid one?”, I think proof-relevant mathematics has a much better answer to the question you claimed to answer “What exactly is a proof?”
(By the way, I highly reccomend Andrej Bauer’s answer to anyone interested in eloquent prose about why proof-relevant mathematics and homotopy type theory are interesting.)