Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

When are two proofs essentially the same? (2007)

gowers.wordpress.com

Post reply on HN
Print view View original

61–70 of 111 posts

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

#61

Post by SkiFire13 »

pkoird wrote: post #30
ColinWright wrote: post #5

Earlier quoted context omitted.

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

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

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

#62

Post by andrewla »

winwang wrote: post #25
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).

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.

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

#63

Post by Jtsummers »

naniwaduni wrote: post #60
Jtsummers wrote: post #58

Earlier quoted context omitted.

Can you show a O(n log n) algorithm with tail calls but not TCO that's O(n) after being optimized with TCO?

Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames.

> Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames.

There are two principal ways of applying asymptotic analysis to algorithms: time or memory used. In both, your procedure is O(n) without TCO. With TCO it is O(n) for runtime (though further optimization would reduce it to O(1) since it's just the constant function 0, but TCO alone doesn't get us there) and O(1) for space since it would reuse the same stack frame.

What O(log n) addresses do you need to hold the stack frames when there are O(n) stack frames needing O(n) addresses (without TCO, which, again, reduces it to O(1) for memory)?

Also, regarding "without tail calls", your example already has tail calls. What do you mean by that?

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

#64

Post by VirusNewbie »

colechristensen wrote: post #27
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 te…

Why not make this rigorous and actually quantify how similar proofs are? I assume this could be done.

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

#65

Post by WCSTombs »

> Is it ever possible to give a completely compelling argument that two proofs are genuinely different?

I think in some cases, we can. Sometimes one of the proofs generalizes better than the other because it uses strictly fewer assumptions. It seems fair to say those would have to be inequivalent.

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

#66

Post by qubitly »

Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome: the path taken, the relationships it establishes, and the concepts it explores are as fundamental as the conclusion itself. Perhaps it’s time to view mathematics not just as calculation, but as a real act of knowledge that in its diversity deepens our grasp of reality

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

#67

Post by red_trumpet »

qubitly wrote: post #66

Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome:…

The result of a prove is a theorem. I don't see any claim in the article that any two proofs of the same theorem are essentially the same?

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

#68

Post by zeroonetwothree »

Jtsummers wrote: post #63
naniwaduni wrote: post #60

Earlier quoted context omitted.

Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames.

> Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames. There are two principal ways of applying asymptotic analysis to algorithms: time or memory used. In both, your procedure is O(n) without TCO. With TCO it is O(n) for runtime (though further optimization would reduce it to O(1) since it's just the constant function 0, but TCO alone doesn't ge…

I assume they mean the size of the address is log n, since there are >n addresses.

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

#69

Post by colechristensen »

VirusNewbie wrote: post #64
colechristensen wrote: post #27

Earlier quoted context omitted.

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

Why not make this rigorous and actually quantify how similar proofs are? I assume this could be done.

You would need a rigorous way to encode proofs likely akin to Gödel numbering or at least something related to automated theorem proving and then add on transformation mechanisms and then rigorously prove that all proofs have transforms from one to the other.

I strongly assume this would be hard.

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

#70

Post by Dylan16807 »

zeroonetwothree wrote: post #68
Jtsummers wrote: post #63

Earlier quoted context omitted.

> Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames. There are two principal ways of applying asymptotic analysis to algorithms: time or memory used. In both, your procedure is O(n) without TCO. With TCO it is O(n) for runtime (though further optimization would reduce it to O(1) since it's just the constant function 0, but TCO alone doesn't ge…

I assume they mean the size of the address is log n, since there are >n addresses.

If we don't treat almost all integers in an algorithm as fixed size then the analysis gets really messy and annoying in a way that has nothing to do with real computers.

And if the algorithm actually did anything with the value that made it grow or shrink with the recursion, the TCO version would stop being O(n) under such a framework. This only works because it's passing 0 around every iteration. And this probably already applies to the TCO version's flow control depending on how you expect to run it.

Post reply on HN