A new proof of Euclid's Theorem (2006) • Hacker News Board

Re: A new proof of Euclid's Theorem (2006)

#21

Post by shasta » Tue, Jan 12, 2016, 7:18 PM UTC

Chinjut wrote: post #20

shasta wrote: post #19

Earlier quoted context omitted.

From the article: The proof just given is conceptually even simpler than the original proof due to Euclid, since it does not use Eudoxus’s method of“reductio ad absurdum,” proof by contradiction. And unlike most other proofs of the theorem, it does not require Proposition 30 of Elements (sometimes called “Euclid’s Lemma”) that states: if p is a prime and p|ab, then either p|a or p|b. Moreover, our proof is constructi…

The article makes suggestions here about the classic proof which aren't true. Euclid's proof of the infinitude of the primes was not phrased in terms of an overarching reductio ad absurdum (and even had it counterfactually been, mathematicians would've long ago been able to trivially rephrase it so as not to be, showing "For any finite set of primes, there is some further prime" directly). And the classic proof of th…

Yeah, I already edited my post. I agree with you.

Re: A new proof of Euclid's Theorem (2006)

#22

Post by CurtMonash » Tue, Jan 12, 2016, 7:32 PM UTC

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not.

When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and synthetic set of axioms to construct a example.

Basically, the axioms were:

"All As are also Bs" "All As are also Cs" "All Bs are also Ds" "All Cs are also Ds"

and the theorem was

"All As are also Ds"

Re: A new proof of Euclid's Theorem (2006)

#23

Post by danharaj » Tue, Jan 12, 2016, 7:38 PM UTC

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

Sure.

Theorem: There exists an even natural number.

Proof 1:

  2. ∎

Proof 2:

  4. ∎

Re: A new proof of Euclid's Theorem (2006)

#24

Post by Chinjut » Tue, Jan 12, 2016, 7:38 PM UTC

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

Yes; putting essentially the same example another way, we might feel intuitively that there are two separate proofs of the propositional theorem that "B AND C" implies "B OR C".

Edit: Or, following up on danharaj's framing, we might feel intuitively that there are two separate proofs of "The set {B, C} is inhabited".

Re: A new proof of Euclid's Theorem (2006)

#25

Post by zingermc » Tue, Jan 12, 2016, 7:41 PM UTC

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D.

Very cool example!

Re: A new proof of Euclid's Theorem (2006)

#26

Post by danharaj » Tue, Jan 12, 2016, 7:52 PM UTC

zingermc wrote: post #25

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

A / \ v v B C \ / v D That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D. Very cool example!

It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways that are not equivalent. Or, you could have two proofs that are equivalent in two ways whose equivalence can be proved, but maybe also in more than one way. You can iterate equivalences of equivalences in such a logic and equality becomes a significantly richer concept.

The study of such mathematical structures is the study of what is called an (infinity,1)-topos.

Re: A new proof of Euclid's Theorem (2006)

#27

Post by Chinjut » Tue, Jan 12, 2016, 7:58 PM UTC

danharaj wrote: post #26

zingermc wrote: post #25

Earlier quoted context omitted.

A / \ v v B C \ / v D That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D. Very cool example!

It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways that are not equivalent. Or, you could have two proofs that are equivalent in two ways whose equivalence can be proved, but maybe also in more than one way. You can iterate equivalences of equivalences in such a logic and equality becomes a significantly riche…

For readers who aren't already familiar with this, I'll note that this is in large part what Homotopy Type Theory is about making easy to work with. http://homotopytypetheory.org/book/ is a good introduction.

Re: A new proof of Euclid's Theorem (2006)

#28

Post by danbruc » Tue, Jan 12, 2016, 8:05 PM UTC

zingermc wrote: post #25

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

A / \ v v B C \ / v D That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D. Very cool example!

One could argue that the proof is just that all As are Xs where all Xs are Ds and therefore all As are Ds. This factors out the detail of choosing one path over the other. You have of course still to show that such an X exists and can use either pair of the axioms establishing this but as far as this proof is concerned both axiom pairs are really equivalent. So are this really two different proofs? How would one define equivalence between proofs to begin with? Isomorphic graphs of applied derivation rules?

Re: A new proof of Euclid's Theorem (2006)

#29

Post by IngoBlechschmid » Tue, Jan 12, 2016, 8:07 PM UTC

obastani wrote: post #16

phasmantistes wrote: post #13

Earlier quoted context omitted.

That's not really an accurate representation of the old proof. You've turned it around to make it look like the new one, but that's not how it is originally laid out at all. The fundamental problem (for constructivists) with Euclid's proof is that it assumes the existence of a set of all primes, and then proves that that set is incorrect (either contains a composite, or doesn't contain at least one specific prime). S…

I think the point is you can easily remove the "deficiencies" of Euclid's proof. Basically, say: let p_1, ..., p_n be the first n primes. We can construct a new prime by examining p_1...p_n + 1. This process can be continued indefinitely. In fact, I think the statement "this process can be continued indefinitely" is quite misleading -- to formalize this, I think you need proof by contradiction. So, the difference is…

There a ways to formulate "the infinity of the prime numbers" without any recourse to a previously-constructed set of all prime numbers (or even all natural numbers). Two such ways are:

1. "For any natural number n, there is a prime number greater than n."

2. "For any natural number m, and for any list of m prime numbers p_1, ..., p_m, there exists a prime number not on that list."

Both statements have a perfectly fine constructive proof. The second statement is more or less precisely what Euclid proved. The first statement follows from the second one with a bit more work.

Re: A new proof of Euclid's Theorem (2006)

#30

Post by robinhouston » Tue, Jan 12, 2016, 8:13 PM UTC

CurtMonash wrote: post #22

This discussion illustrates an interesting point -- it can be a little tricky to judge whether two proofs are actually "different" or not. When I was a grad student I interrupted a study session to raise the simple question -- can a theorem really have two different proofs? We all thought the answer was yes, but the discussion went on for several minutes until I settled it by contriving a stupidly simple and syntheti…

From the point of view of category-theoretic logic – which is the area I did my PhD in – there is a sense in which all classical proofs are equivalent.

Roughly speaking, the argument goes like this. Intuitionistic propositional logic can be modelled by cartesian closed categories. (The canonical reference for this correspondence is the book “Introduction to Higher Order Categorical Logic” by Lambek and Scott.) But a lemma due to André Joyal shows that, if a cartesian closed category is a model of classical logic (i.e. validates the law of excluded middle), then there is at most one proof of any given implication: in the jargon, the category is a poset.

See http://mathoverflow.net/a/43285/8217 for a proof.