When are two proofs essentially the same? (2007) • Hacker News Board

Re: When are two proofs essentially the same? (2007)

#21

Post by justinpombrio » Tue, Oct 29, 2024, 4:05 PM UTC

pkoird wrote: post #2

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…

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

Re: When are two proofs essentially the same? (2007)

#22

Post by js8 » Tue, Oct 29, 2024, 4:06 PM UTC

Twisol wrote: post #17

lupire wrote: post #13

Earlier quoted context omitted.

Asymptotics and stability are different theorems. 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.

> An algorithm is not a proof. 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…

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

Re: When are two proofs essentially the same? (2007)

#23

Post by Someone » Tue, Oct 29, 2024, 4:10 PM UTC

pkoird wrote: post #2

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…

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.

Re: When are two proofs essentially the same? (2007)

#24

Post by pkoird » Tue, Oct 29, 2024, 4:12 PM UTC

Twisol wrote: post #10

pkoird wrote: post #2

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…

I disagree with this on two points. 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 importan…

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

Re: When are two proofs essentially the same? (2007)

#25

Post by winwang » Tue, Oct 29, 2024, 4:21 PM UTC

pkoird wrote: post #2

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…

Two programs which are semantically equivalent are not simply the same. See: bubblesort vs mergesort. (Yes I'm relying on curry-howard isomorphism here).

Re: When are two proofs essentially the same? (2007)

#26

Post by gus_massa » Tue, Oct 29, 2024, 4:22 PM UTC

Y_Y wrote: post #16

lupire wrote: post #8

Earlier quoted context omitted.

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 monogra…

Neglect considerations of homotopy at your peril!

Yep.

If you can go from A to C by B or B' and all the place is a nice grass field they are probably equivalent.

But if between B anb B' there is an active vocano, most people would call the paths different.

Re: When are two proofs essentially the same? (2007)

#27

Post by colechristensen » Tue, Oct 29, 2024, 4:24 PM UTC

Xcelerate wrote: post #20

One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a…

>I agree with pkoird's point that philosophically, two correct proofs of the same theorem should be considered "the same". Any theorem is ultimately a property of the natural numbers themselves along with the various paths that lead there from the axioms (since all proofs are essentially a finite sequence of Gödel numbers).

As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y.

The article seems to be digging at the existence of a few categories of proofs

* proofs that are trivially transformed into one another

* proofs that use substantially similar arguments that don't necessary have a direct transformation

* proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof

So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"?

One extreme is "the slightest change in wording makes a proof unique"

The other extreme is "any two proofs of the same concept are by definition the same proof"

I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements.

What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.

Re: When are two proofs essentially the same? (2007)

#28

Post by Twisol » Tue, Oct 29, 2024, 4:36 PM UTC

js8 wrote: post #22

Twisol wrote: post #17

Earlier quoted context omitted.

> An algorithm is not a proof. 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…

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

Re: When are two proofs essentially the same? (2007)

#29

Post by 6gvONxR4sf7o » Tue, Oct 29, 2024, 4:36 PM UTC

Xcelerate wrote: post #20

One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a…

It seems like in your first part, you're saying that proofs are the same as their normalized proofs, up to some rewriting system. So like how we say 3-2 is the same as 1, basically, or (more interestingly) saying that x-x is the same as zero, or that e^(i pi (2n+1)) is the same as -1. Yes, they can be reduced/normalized to the same thing, but in basically any system with terms, `reduction(term)` is not always the same as `term`, And 'a sequence of term transformations' is a common proof method.

There's obviously a sense in which they're the same, but at the proof level, I would be surprised if that's a particularly useful sense, because the whole point of a proof is that it's the journey, not the destination. Even within the same "level," in your terms.

Re: When are two proofs essentially the same? (2007)

#30

Post by pkoird » Tue, Oct 29, 2024, 4:38 PM UTC

ColinWright wrote: post #5

pkoird wrote: post #2

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…

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". I'd argue that this is not the case.

Not quite.

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.