If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of different "abstractions", but it just seems to me that these abstractions should be equivalent if one were willing to unravel it all to a certain degree. Essentially, all proof is, is a statement that says "this is true" and no matter which language you use to say it, you are saying the same thing.
This is like saying that if I walk out of my house, turn right, and walk 10 minutes to the local food store, it's the same as coming out of the house, turning left, and walking 15 minutes around the block. The destination is the same, so surely these are "the same".
If we consider that we are trying to prove "you can reach the local food store from your house" then starting from either side would consist of two proofs by example. And for sure these are different paths one is taking and should be different! But if you consider deeply, both of these proofs are implicitly encoding same information about the space between your house and the local store:
1) there is continuous space between your house and the store i.e. the store is reachable from your house. (as opposed to your house being in on an island and you not being able to swim)
2) you can traverse two points in a continuous space.
What I wanted to opine was merely the fact that since all proofs use logic, assuming certain premise, all theorems about a certain statement being true must be reducible to a single irreducible logical chain of argument. It is true that we use different abstractions that have relevant meaning and ease in different contexts but since all of our abstractions are based upon logic in the first place, it does not seem outlandish to me to think that any logical transformation and subsequent treatment between two proof structures should inherently encode the same facts.
The path example is extremely fertile ground for this kind of discussion! It is definitely true that both paths encode the information that one's house is connected to the local store. But is that all they encode? Homotopy theory is all about the different paths between two points, and it tells us some quite interesting things! In particular, if you have two paths from point A to point B, you can ask: can you smoothly animate an image of the first path into an image of the second, such that every still frame in-between is also a legitimate path? (If you can't, that tells you that there's some form of hole in between them!)
In the house/store example, a path is also a witness to the fact that, if you perform a road closure anywhere not on the path, then connectivity is preserved. Simply stating that the two points are connected doesn't tell you whether it's safe to close a road! Moreover, taking the two paths together tells you that performing a single road closure that only affects one of the paths will still leave a route you can take.
In both examples, if the paths were logically interchangeable, you wouldn't be able to get more information out of the both of them than you could from just one. But because they aren't equivalent -- because each contains some information that the other does not -- we can deduce more from both together than from either individually.
> all theorems about a certain statement being true must be reducible to a single irreducible logical chain of argument.
Why is this necessarily true? We know that true statements in topology (for example) don't all reduce down to being equivalent (eg if I have a loop that goes through the ring of a donut/toroid it doesn't reduce the same as if I have a loop on the surface of the donut/toroid so establishing facts about one wouldn't tell me facts about the other). So how do we know that statements in logic reduce? Could the space of logical statements not have topological characteristics like that?
You are being too literal -- I was providing an analogy, not an example.
Also:
> ... all theorems about a certain statement being true must be reducible to a single irreducible logical chain of argument.
Citation needed ... I have no reason to believe this is true.
But here's an example of two proofs.
Proving sqrt(2) is irrational.
Proof 1:
Every rational number has a finite Continued Fraction representation. But the normalised Continued Fraction representation of sqrt(2) is [1;2,2,2,...], which is infinite. Since this is infinite, sqrt(2) is irrational.
Proof 2:
Consider integers a and b, and suppose 2(b²)=a². Consider the prime decompositions of a and b, and count how many times "2" turns up on each side. It's odd on the left, it's even on the right, so this cannot happen. Therefore we can never have integers a and b with 2(b²)=a². Therefore we can't have 2=(a²)/(b²)=(a/b)². So any fraction when squared cannot equal 2, so sqrt(2) is irrational.
> But if you consider deeply, both of these proofs are implicitly encoding same information about the space between your house and the local store
That is only _some_ of the informations that they encode, and particularly informations shared by both proofs, but that it not the only information they encode! The exact way to reach the local food store is also some information, and they encode different ways, hence different informations.
> What I wanted to opine was merely the fact that since all proofs use logic
Note that there's no single logic! There are at least two big logics, classical and constructive/intuitionistic, each with their own variants.
For example a proof by contradiction is valid in classical logic but not in constructive one. It would give you a proof that there must be a way to reach the local store without giving you the way to reach it. Would it still count as the same proof as the other two for you? It doesn't encode how to reach it, so for some it's not even a valid proof.
There's a simple mechanical transformation from one path to the other.
As a proof that "the store is reachable, they are essentially the same if it is already known that you live on a "block" with the store" . If it is not known that you live on a block, then the second proof together with the first gives a much deeper result, proving that you do live on a block. That makes a second proof valuable, but in the monograph of history, it is most parsimonious to make the block proof and the note how it implies to trivially distinct ways of reaching the store.
First, oftentimes the interest in proving long-standing, difficult mathematical problems is because we hope a proof will demonstrate new tools for tackling similar problems. In that sense, the exact content of a proof is quite important. Not to mention, there is value in having multiple proofs that each demonstrate quite different toolkits. Mere truth is not often the most important thing -- after all, mathematicians can (and do!) take certain propositions as premises of downstream work. If we discover a proof for one of those premises, that just means we can drop the premise from downstream work. Not having a proof doesn't block us from making use of the proposition anyway.
Second, sometimes the content of the proof is relevant formally. A sibling comment gave an example in terms of paths between two points; it is often the case that you care not only that the points are merely connected, but you also have a preference for which path is taken. Or, you can do an analysis of the paths themselves, and determine their length or average furthest distance from the nearest McDonalds. A path is "just" a proof of connectivity, but the individual paths can be quite distinct when studied themselves. Less abstractly, a constructive proof will yield an algorithm that can be performed, and we know quite well that the variety of sorting algorithms (that "merely" prove that "all lists are sortable") actually vary in quite important ways, including asymptotics and stability.
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.
An algorithm is not a proof. It is a technique for proof.
Two algorithms can be different, while not being meaningfully different profs that a list is sortable.
To the extent that they are different, they proof different theorems, such as "list can be sorted in O(f) time" for an f of interest.
That is an opinion that many do not share. FWIW, I framed my response as an opinion; you gave yours as a blanket statement. It is not wrong to treat algorithms as valid proofs.
In a dependent type theory, propositions are represented as types; the proposition that "all lists can be sorted" could be represented represented as the type "forall (t : Type) -> (le : Ordered t) -> forall (xs : List t) -> exists (ys : List t). (Increasing le ys, PermutationOf xs ys)". A proof of this proposition is exactly a program (algorithm) with that type; the sorted list is the `ys` component of the returned existential product. Yet the inhabitants of this type are not graded by asymptotics or stability; any sorting algorithm will do.
In a setting where inhabitants of the above type are distinguishable, you could then write proofs of asymptotics or stability against individual algorithms. That is, the proofs of the sorting proposition are themselves the subjects of subsequent propositions and proofs thereof.
> It is not wrong to treat algorithms as valid proofs.
I think that's what PP meant, i.e. if you want to differentiate between sorting algorithms in terms of efficiency, you somehow should encode this demand into the types (specification).
You can do that, yes. My argument is that you don't have to do that -- you can prove asymptotics or stability after the fact, having previously only given an algorithm as a proof of sortability.
Putting these properties in the specification assumes you already know (or suspect) that your algorithm has these properties; then you are simply verifying what you knew. If you develop your algorithm first, then want to analyze it in terms of (say) asymptotics, then not only is it far too late to change the type, you don't even know what the asymptotics are yet. You'd still like to treat the algorithm formally in order to determine those asymptotics, but since you don't know them yet, the algorithm can't inhabit a type that states those asymptotics outright.
Two programs which are semantically equivalent are not simply the same. See: bubblesort vs mergesort. (Yes I'm relying on curry-howard isomorphism here).
I don't know why this hasn't been voted to the top. Curry-Howard isomorphism is a hell of a bludgeon to apply here but it makes for a very straightforward and obvious refutation of the parent post.
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 be shown to be equal to the triangle's other two interior angles. (Try drawing it out.)
Second proof: start at one side of the triangle and walk around it. By the time you return to where you started, you must have turned 360 degrees. Thus the sum of the exterior angles is 360 degrees. Each interior angle is 180 minus the corresponding exterior angle, and there are three of them, so calling the interior angles A, B, C and the exterior angles A', B', C' we have A'+B'+C' = 360 implies (180-A) + (180-B) + (180-C) = 360 implies 540 - A - B - C = 360 implies 180 = A + B + C.
2. Prove that the sum of the first N numbers is N(N+1)/2.
First proof: sum the first and last number to get 1 + N, then the second and second-to-last to get 2 + (N-1) = 1 + N, repeating until you get to the middle. There are N/2 such pairs, giving a total of (1 + N)N/2. (This assumed that there were an even number of terms; consider the odd case too.)
Second proof: proceed by induction. For the base case, it's true for N=1 because 1*2/2 = 1. For the inductive case, suppose it's true for N-1. Then 1 + 2 + ... + N-1 + N = (1 + 2 + ... + N-1) + N = N(N-1)/2 + N = N(N-1)/2 + 2N/2 = N(N+1)/2.
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 thing with the first one summing the numbers from extremities and the second one summing 1...N-1 first and then the last. I'd argue that if addition were not commutative, you may have obtained different results.
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.
Have you not actually built the same proof via induction in both cases with one of them starting from the middle and subsequently including left and right terms at a unit away (you actually do it in reverse but the crux still holds)? Such that S[0] gives you (N+1)/2 and S[(N-1)/2] gives you the total sum.
The argument would be like S[i] = (2i-1)(N+1)/2 only you'd be proving it using induction i.e. given S[i-1], finding S[i].
All it ever matters for this problem is that to prove it as such, you somehow have to add up all of the numbers. The "different" proofs you presented are actually the same since for addition, the order of operation does not matter due to associative and commutative properties. A good question would be to see if any of the proofs still remain valid when either of these properties are removed from an operation.
You're handwaving, but I think there is a middle-ground in this proof:
Sum(i=1..n, i)
= Sum(i=1..n/2, i) + Sum(i=1..n/2, n+1-i)
= Sum(i=1..n/2, n+1)
I'm still interested in the general question, of whether some proofs have big gaps between them. The more complex the proofs, the more obvious this would be; my examples are unfortunately simple. Something like proving the fundamental theorem of algebra using Rouche's Theorem (complex analysis) vs. field theory. But I don't know enough math to compare those.
How abut the following proofs that sqrt{2} is irrational.
1. If 2=a^2/b^2 with a and b relatively prime then a^2=2b^2 so a is even, and, letting a=2c, b is also even a contradiction.
2. Use the lemma that a positive real r is rational if and only if there is a positive integer b such that br is an integer. (Proof left to the reader.) if sqrt{2} is ration then there is an integer b such that bsqrt{2}=a for some integer a. Let b be the smallest such integer. Then, if c=b(sqrt{2}-1) then c is smaller than b, c=bsqrt{2}-b is an integer, and sqrt{2}c=sqrt{2}b(sqrt{2}-1)=2b-b*sqrt{2} is an integer, a contradiction (this uses infinite descent).
3. Use the theorem that if x, y, and n are positive integers such that x^2-ny^2=1 then sqrt{n} is irrational, and apply with n=2, x=3, y=2.
Proof of theorem.
a. If x^2-ny^2=1, then using (x^2-ny^2)^2=(x^2+ny^2)^2-n(2xy)^2 to show that there are arbitrarily large solutions to x^2-ny^2=1.
b. If n=a^2/b^2 then 1=x^2-(a^2/b^2)y^2 so b^2=b^2x^2-a^2y^2=(bx+ay)(bx-ay)>=bx+ay>bx so b>x but this contradicts the existence of arbitrarily large x.
Theorem: there are 500,000 odd integers between zero and a million.
Proof #1: there ar no odd integers between zero and 1 (inclusive), 1 is odd so there is 1 odd integer between zero and 2, 2 is even so there is 1 odd integer between zero and 3, 3 is odd so there are 2 odd integers between zero and 4, …, 999,998 is even so there are 499,999 odd integers between zero and 999,999, 999,999 is odd so there are 500,000 odd integers between zero and 1,000,000. QED.
Proof #2: this is a specific case of “there are n odd integers between zero and 2n (exclusive)”. (proof of the more general theorem). Picking n to be 500,000, the theorem follows.
I think most people would call those two proofs different.
I don't think this is true because a proof does more than state a conclusion. It establishes a true path from some premises to that conclusion. Sometimes that path continues.
For example if you had a general constructive proof that there were infinitely many prime numbers it should be a simple matter to alter it a bit and prove the twin prime conjecture wouldn't it?
In general a constructive proof and a non-constructive proof of some fact (say proof by contradiction) are fundamentally different in terms of where you can go with the proof.
A proof is not a statement that something is true, but a demonstration that it is true.
Are you familiar with the proofs-as-programs idea?
The uh, something isomorphism? Idr the name.
Not all programs that implement a function are the same.
When you boil things down to the fundamental steps of the logic you are working on, you needn’t get the same thing.
For one thing, it may be that axioms A and B suffice to prove Z, and that axioms B and C suffice to prove Z, but that B alone doesn’t, and that A and B doesn’t prove C and that B and C doesn’t prove A.
So, the proofs using A and the proofs using C are certainly different.
I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type.
As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).
There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.
We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729.
Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves.
The choice of types already reflects what we want to study.
Hm. Take for example formalization in Calculus of Constructions (Coq, Lean). What you propose is essentially beta-equivalence of the underlying lambda calculus terms.
However, this is not without problems (undecidability aside). Different CoC formalizations can use, for example, different LC representations of natural numbers (Church numerals, binary..) or other basic types, such as pairs.
Does that mean that proof using Church numerals and proof using binary numerals are different? Intuitively, I don't think so, yet they are according to above definition.
Another example. One can embed classical propositional logic into intuitionistic one using translation of LC terms (basically continuation-passing style transform). Is the translated proof the same or different? It operates on different terms and is thus different as a program.
I think the fundamental problem is the idea that there is some universal and absolute equivalence relation between proofs. Rejecting that leads to accepting equivalence relative to the type of the proposition. (I think you can get some absoluteness back using univalence axiom, but I don't comprehend that.)
It isn’t clear to me why the encoding of the natural numbers would come up. I would have thought that some statement about the natural numbers would involve some type, considered as the type of natural numbers, which I suppose if you construct it from other simpler primitives would have some kind of encoding,
But, if the proof uses only uses the terms of that type through the use of the constructors etc. associated with that type, you wouldn’t have multiple proofs which differ only by the encoding, and belonging to the same type (proposition), as the encoding would just be whatever encoding is used for the type of integers used.
It seems likely that I’ve misunderstood what you meant.
Still, if you have two different natural numbers objects, there’s an isomorphism between them… I guess one could use this to translate between proofs for one and proofs for the other, but I don’t know if translating and then translating back would yield the original proof.
I wouldn’t be surprised if by default it doesn’t.
It wouldn’t surprise me if there is a way to “make it the same” while still keeping other proofs distinct, though.
I suppose one could make some sort of quotient type?
Also, for (intuitionistic) existential statements, the proof can almost be seen as just the thing claimed to exist along with a witness that it is that thing.
So, if you say, “for all x:X, there exists y:Y, such that P(x,y)” , then two proofs might differ by giving two different functions x:X->(y:Y,p:P(x,y)) which, could be regarded as different if the X->Y part is different without considering whether the p part is different.
Maybe if one e.g. required equality types to be sub-singletons (i.e. if p,q : Eq(Nat,x,y) then p is q ) but allowed other propositions to have multiple distinct elements, that could be, something?
I appreciate your comment but I think you're overcomplicating it for yourself. (And btw I doubt I know more about this than you.)
You say:
"It isn’t clear to me why the encoding of the natural numbers would come up. I would have thought that some statement about the natural numbers would involve some type, considered as the type of natural numbers, which I suppose if you construct it from other simpler primitives would have some kind of encoding."
OK, so let's say we have an agreement, that your representation for the type of natural numbers is practically - from a typing viewpoint - identical to my representation for the type of natural numbers. So then we don't have to worry about the encoding. And it makes sense to do this for all the primitive types we are using.
But then consider your proposition "for all x:X, there exists y:Y, such that P(x,y)". This proposition is itself a type, which is constructed from primitive types. So why would you here, all of sudden, want to distinguish between different proofs, or rather, representations of this particular type?
I think, if we both accept proposition-as-types paradigm, then I am reasoning backwards from it. If the structure of two different proofs of the same (propositional) type matters (whatever the reason), not just existence of these proofs, why shouldn't it matter with the primitive types? It implies that we need to come to an agreement what primitive types we are using, because their structure might matter, too.
And that's why I said - you effectively want your "universal proof equivalence" to be the beta-equivalence of underlying lambda terms, because lambda calculus is a mechanism how we construct the complex types from primitive ones (not all constructions are valid though, there are typing constraints). But, as I already explained, it doesn't really give you a grounding, because there are multiple ways to define primitives in lambda calculus which cause the terms not to be beta-equivalent. So you have to care about having such agreement how you implement these primitives. Hopefully this clears up where it comes from.
But having that agreement in itself then limits what you can prove (in particular, you cannot prove equivalence of different representations, since you're already taking it as an axiom), so you don't really want to have such an agreement. That's why I believe the only sensible way out is to propagate the proof indifference "upwards" - even for complicated types (practically usable propositions), the actual representation shouldn't matter.
No worries, though. If you want the representation to matter, you would do the same thing you do in lambda calculus - you choose some encoding of lambda terms, and take an interpreter for this encoding which implements beta-reduction. When interpreting an encoded lambda term, you can discern different implementations (for example, their complexity properties) of otherwise beta-equivalent lambda terms. Mathematically, this gives a different theory. (Also note there is no reason for your encoding to be working with just lambda abstraction and application as primitives, you can encode different lambda terms in different ways, if you need to. That's what combinatory logic does, it lets you use an arbitrary basis of primitives.)
A Proof is not a statement. A theorem is a statement.
Proofs are usually not completely formal or even formalizable. Math is not completely well founded.
"Unravelling it all the way" might be an open research project, or a new conjecture directly inspired by the second, apparently different proof. Showing these two profs to be equivalent might depend on a major new idea that happens after the two proofs are createdm
This is hinted at in the OP discussion of Terry Tao.
yes : if two discrete semiotic symbolic networks point to the same signified value they are the same in the way two different poems with the same meaning are the same. which is to say they are unique but have the same meaning.
