4 ms·

Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states

Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states and thus a path in a sort-of-metric space. Two proofs could said to be similar if their paths are "close" in that sort-of-metric space. Of course, you're left with the question of how close is close and whether "close" means close at one intermediate point or many. Moreover, mathematicians often like proofs that are more "cohesive" than just sequences of manipulations. So the question with real world would probably be a matter of mathematical taste as well as objective measures.

setopt 2y ago
It’s also hard to prove that a statement definitely lies in the “space of true statements”. Moreover, whether a proof assumes “A = B” or “B = C” can make them closer together or further apart in such a space depending on whether it is established that “A = C” or not, which also makes it tricky to establish rigorously.
- chongli 2y ago
  If you haven’t established that A = B and B = C implies A = C then you haven’t proven that = is an equivalence relation on that space including A, B, and C. Unless you’re going to prove it I would go so far as to call it an abuse of notation to continue using = when you mean some other relation where transitivity does not necessarily hold.
  - setopt 2y ago
    What I mean is that at the time something is proven, it might not be clear that those assumptions are equivalent. Like assuming at the start of a proof that the Axiom of Choice holds vs that Zorn’s lemma holds. That those two proofs are “close” requires that you know it’s already proven that they are equivalent. In that sense, I believe whether proofs should be considered close or not is more subjective than objective, as it depends on the previous knowledge of the reader. My point above is that one mathematician might assume A=B and another might assume A=C, and both prove the same things. That doesn’t mean they know that always B=C even if it’s true, in which case it’s hard to say whether the proofs are close.

setopt 2y ago

It’s also hard to prove that a statement definitely lies in the “space of true statements”. Moreover, whether a proof assumes “A = B” or “B = C” can make them closer together or further apart in such a space depending on whether it is established that “A = C” or not, which also makes it tricky to establish rigorously.

chongli 2y ago
If you haven’t established that A = B and B = C implies A = C then you haven’t proven that = is an equivalence relation on that space including A, B, and C. Unless you’re going to prove it I would go so far as to call it an abuse of notation to continue using = when you mean some other relation where transitivity does not necessarily hold.
- setopt 2y ago
  What I mean is that at the time something is proven, it might not be clear that those assumptions are equivalent. Like assuming at the start of a proof that the Axiom of Choice holds vs that Zorn’s lemma holds. That those two proofs are “close” requires that you know it’s already proven that they are equivalent. In that sense, I believe whether proofs should be considered close or not is more subjective than objective, as it depends on the previous knowledge of the reader. My point above is that one mathematician might assume A=B and another might assume A=C, and both prove the same things. That doesn’t mean they know that always B=C even if it’s true, in which case it’s hard to say whether the proofs are close.