back

by pkoird·1y ago·view on hn ↗
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).

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