4 ms·
One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can
by Xcelerate 2y ago
One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a halting state).
But that's too difficult in some cases. Most of the Goodstein sequences reach extraordinarily high values before coming back down. How can we prove they all eventually reach 0? Even at small values of n, the sequence length of G(n) requires something on the order of the Ackermann function to specify bounds. We can't inspect these sequences directly to prove whether they reach 0. Instead we create a "parallel" sequence to a Goodstein sequence. Then we prove there exists an algorithm that maps from each item in the parallel sequence to an item in the Goodstein sequence such that both sequences are well-ordered and decreasing. If the parallel sequence reaches 0, then so does the Goodstein sequence. You could think of this as one Turing machine computing the configurations of another Turing machine or perhaps one branch of a tree "cross-predicting" the items along another branch. You aren't just following the branch to its end. In this sense, the proof occurs at a higher "level".
This concept is known as ordinal analysis and one can consider the proof-theoretic ordinal of any theory T. If T_1 and T_2 both prove a specific theorem and have the same proof-theoretic ordinal, you could consider the two proofs to occur on the same "level". Interestingly, Peano Arithmetic can prove that any specific Goodstein sequence reaches 0 but not that all Goodstein sequences reach 0—this requires a more powerful formal system. So if you prove a specific sequence reaches 0 using the more powerful system, I would say that's a fundamentally different proof.
- colechristensen 2y ago>I agree with pkoird's point that philosophically, two correct proofs of the same theorem should be considered "the same". Any theorem is ultimately a property of the natural numbers themselves along with the various paths that lead there from the axioms (since all proofs are essentially a finite sequence of Gödel numbers). As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y. The article seems to be digging at the existence of a few categories of proofs * proofs that are trivially transformed into one another * proofs that use substantially similar arguments that don't necessary have a direct transformation * proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"? One extreme is "the slightest change in wording makes a proof unique" The other extreme is "any two proofs of the same concept are by definition the same proof" I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements. What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.
- Xcelerate 2y agoYeah, my first sentence is sort of nonsense the more I think about it... removed it to keep the focus of my comment on different kinds of proofs.
- VirusNewbie 2y agoWhy not make this rigorous and actually quantify how similar proofs are? I assume this could be done.
- colechristensen 2y agoYou would need a rigorous way to encode proofs likely akin to Gödel numbering or at least something related to automated theorem proving and then add on transformation mechanisms and then rigorously prove that all proofs have transforms from one to the other. I strongly assume this would be hard.
- lanstin 2y agoSome sort of Hamming distance in Lean proofs perhaps? Seems unlikely to capture the difference in what a person would say are different proofs tho. And even when people say a proof is different from another one there is usually some notion of "according to our current understanding" with the idea that some further result could show that the apparently unrelated results are aspects of some deeper unity.
- 6gvONxR4sf7o 2y agoIt seems like in your first part, you're saying that proofs are the same as their normalized proofs, up to some rewriting system. So like how we say 3-2 is the same as 1, basically, or (more interestingly) saying that x-x is the same as zero, or that e^(i pi (2n+1)) is the same as -1. Yes, they can be reduced/normalized to the same thing, but in basically any system with terms, `reduction(term)` is not always the same as `term`, And 'a sequence of term transformations' is a common proof method. There's obviously a sense in which they're the same, but at the proof level, I would be surprised if that's a particularly useful sense, because the whole point of a proof is that it's the journey, not the destination. Even within the same "level," in your terms.
- Xcelerate 2y agoMy first sentence didn't make sense and wasn't well-thought-out. Removed it in favor of keeping the discussion about proof-theoretic strength.