I don't think you have disagreed with me. You have advocated that different tools/methods are useful for different problems and may have unique properties that make them interesting in specific contexts. I completely agree and I have not stated anything against it. My opinion, admittedly abstract and stated without proof, was simply that if you have two ways of showing something to be true, they must be logically equivalent (in some sense of the word) if you are willing to dig deep enough. This does not necessarily imply that certain abstractions are not useful on their own, merely that at a certain level, they should represent the same thing.
I fully understand that this is not a concrete argument and I have not stated my opinion with desirable rigor (but the author of the original article does provide a few examples in support). Maybe someone with a better grasp on abstract mathematical concept could convey my arguments better (if they think it's true).
That's a fair response; thanks for taking the time.
I was primarily reacting to this part of your message...
> I'd argue that two correct proofs are always the same.
...with emphasis on the "always". To my eyes, a proof is any object that witnesses the truth of a proposition. The proof can be more than a witness, but to be called a proof, it must do at least that much.
To say that "two correct proofs are always the same" is, to me, to say that proofs can be no more than witnesses of the proposition; to be the same means to be indistinguishable. My argument is that two correct proofs may be distinct in useful ways.
I suppose this discussion depends on what "same" means ("depends on what the meaning of the word 'is' is", heh). Do you mean something other than what I mean? Your use of "logically equivalent" is probably telling -- so, two proofs should have the same deductive power? We often speak of propositions this way, but I'm not sure how to understand that notion on proofs. Terence Tao gives some possible notions of proof equivalence in a comment on the OP [0]; you might enjoy reading them and considering which is closest to your intuitive idea of equivalence :)
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 represent a single terminal symbol i.e. either T (true) or F (false) and s1... and s11... etc. could be different abstractions that have been employed to illustrate the veracity of the statement.
Regardless, both of these abstractions make use of the same Logical rules at each step so you could argue that the logical chain of both P1 and P2 are equivalent in some sense. If you think about it, it does seem obvious though, because if P1 and P2 disagreed with P1 yielding T and P2 yielding F, while using the same set of logical rules, it must be the case that either the logic is not consistent or one or both of the chain has errors.
So now, one could argue that all such correct logical chains (maybe of different lengths) that start with a statement s0 and terminate at a single symbol (say T) should essentially be the same.
s1 -> s2 -> s3 -> ... -> sn
↑................................↓
s0 -> s11 -> s12 -> ...->T
You could also argue that there must be exactly one such chain of the smallest possible complexity (in some sense) and that all other chains should be reducible to this one chain (not sure how).
At the end, I still agree with you in that two correct proofs can be distinct in useful ways but since proofs, to me, are a series of application of logic under certain premise to obtain a terminal symbol, all such logically sound chains must actually correspond to the one fundamental chain that's irreducible (in some sense).
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, one in which I use A and B (but not C) to yield the desired result, and another in which I use B and C (but not A).
In what way can we say that these two proofs are essentially the same? It appears that each uses potentially rather distinct information in order to derive the expected contradiction; it isn't clear how to go from a proof that avoids A to a proof that avoids C in a smooth way.
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!
> 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
Yes, absolutely :) I thought about this framing too, but figured the one I gave above might be more immediately convincing.
I fully understand that this is not a concrete argument and I have not stated my opinion with desirable rigor (but the author of the original article does provide a few examples in support). Maybe someone with a better grasp on abstract mathematical concept could convey my arguments better (if they think it's true).