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.
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.