I was working with a friend writing a paper about the Ship of Theseus, but my friend kept replacing all of my arguments.
When are two proofs essentially the same? (2007)
41–50 of 111 posts
Re: When are two proofs essentially the same? (2007)
#42Earlier quoted context omitted.
I can attempt to semi-formalize it but I'm sure I'd butcher it along the way so feel free to point out anything that doesn't feel correct. Consider a set of premises P that are assumed to be true. Also, consider that we are trying to analyze a statement s0 assuming P. One proof could be of the form: P1: s0 -> s1 -> s2 -> ... -> T/F. Another proof could be of the form: P2: s0 -> s11 -> s12 -> ... -> T/F. Where T/F rep…
Thanks for taking a stab at it! I think I understand the angle you're attempting to take. May I offer a relatively contrived counterexample to poke at this a little more deeply? Suppose I have a proposition that says, roughly, "if A and B and C then contradiction". Furthermore, suppose that A and B together are already contradictory, and B and C together are also already contradictory. Now I can construct two proofs,…
That is a really good question. I suppose you could reduce it further by saying that you want the proof of "A or B". Assuming both true, it suffices to either get a proof for A or for B (of course, this may not be true in general).
Regardless, this is a really good counter-example that will force me to think some more about it. Thanks!
Re: When are two proofs essentially the same? (2007)
#43See Girard, The Blind Spot: Lectures on Logic (2011) for some attempts at tackling this question. (in particular, his "proof nets" attempt to have a canonical form, such that we can identify differently drawn concrete proof nets as representing the same abstract proof)
Re: When are two proofs essentially the same? (2007)
#44Re: When are two proofs essentially the same? (2007)
#45Earlier quoted context omitted.
Some proofs that aren't "essentially the same": 1. Prove that the interior angles of a triangle sum to 180 degrees. First proof: draw a line parallel to one of the triangle's sides passing through its opposite vertex. There are three angles on one side of this line, and they obviously add to 180 degrees because it's a line. One of the three angles is directly one of the triangle's interior angles; the other two can b…
I'm responding to your second example simply because it's easy to argue about. I'd say that both proofs that you have presented are equivalent ways of saying that "since when you sum all the numbers from 1 to N you obtain a number that's N(N+1)/2, therefore, it is true that the sum of numbers from 1 to N is N(N+1)/2". Now, this argument may appear trite but do consider that both of your proofs essentially do the same…
If two programs are equivalent, you can typically show that they're equivalent with a sequence of small refactorings. Replace `x + x` with `2 * x`. Inline that function call. Etc.
Can you do that with these two proofs? What's a proof that's halfway in between the two?
If you can get from one proof to the other with small "refactorings", then I agree that they're fundamentally the same. If you can't---if there's an insurmountable gap that you need to leap across to transform one into the other---then I'd call them fundamentally different. If you insist that two proofs are "essentially the same thing" despite having this uncrossable gap between them, then I suspect you're defining "essentially the same" to mean "proves the same thing", which is a stupid definition because it makes all proofs the same by fiat, and avoids the interesting question.
Re: When are two proofs essentially the same? (2007)
#46Well, 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.
Re: When are two proofs essentially the same? (2007)
#47I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which diff…
I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1)…
On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?
Re: When are two proofs essentially the same? (2007)
#48Well, 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…
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.
Re: When are two proofs essentially the same? (2007)
#49I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which diff…
I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1)…
From complexity analysis we can adopt the concept of polynomial-time reducibility and might define a type of equivalence relation where two algorithms are equivalent only if both are pt-reducible to each other. Intuitively it’s not a sufficient condition for "sameness" – otherwise, for example, all NP-complete problems are the "same" and solvable with the "same" algorithm – but it’s arguably a necessary one.
Re: When are two proofs essentially the same? (2007)
#50Earlier quoted context omitted.
I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1)…
On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?
Tail call optimization does not turn O(n) algorithms into O(1) algorithms unless you're talking about the space used and not the runtime.