3 views

Skip to first unread message

May 8, 2005, 8:57:31â€¯AM5/8/05

to

While Euclid's classic proof that there are infinitely many primes is

easy to understand intuitively, I found the following proof simpler to

formalize for an automated proof verifier. (Specifically, this proof

avoids the product of a hypothetical finite set of all primes, which I

found cumbersome to work with.)

easy to understand intuitively, I found the following proof simpler to

formalize for an automated proof verifier. (Specifically, this proof

avoids the product of a hypothetical finite set of all primes, which I

found cumbersome to work with.)

Here is the proof:

For any natural number n, the smallest divisor (greater than 1) of n!+1

is a prime greater than n. Hence there is no largest prime.

As simple as it is, I was unable to find a published reference for this

proof. Is it a known proof?

--

Norm Megill http://public.xdi.org/=nm

May 8, 2005, 8:59:00â€¯AM5/8/05

to

Norman Megill <n...@see.signature> writes:

> While Euclid's classic proof that there are infinitely many primes is

> easy to understand intuitively, I found the following proof simpler to

> formalize for an automated proof verifier. (Specifically, this proof

> avoids the product of a hypothetical finite set of all primes, which I

> found cumbersome to work with.)

There is no such set in Euclid's proof.

> As simple as it is, I was unable to find a published reference for this

> proof. Is it a known proof?

Yes, it's a common variant.

May 8, 2005, 9:16:39â€¯AM5/8/05

to

Torkel Franzen wrote:

> Norman Megill <n...@see.signature> writes:

>

>>(Specifically, this proof

>>avoids the product of a hypothetical finite set of all primes, which I

>>found cumbersome to work with.)

>

> There is no such set in Euclid's proof.

I used Euclid's proof from _The Book of Prime Number Records_, which

starts off: "Suppose that p_1 = 2 < p_2 = 3 < ... < p_r are all the

primes." This specifies a function from {1,...,r} onto a hypothetized

finite set of all primes. Whether this is what Euclid intended is

another matter - set theory not having been invented yet. :) My goal

was simply to formalize it under modern set theory.

>>As simple as it is, I was unable to find a published reference for this

>>proof. Is it a known proof?

>

> Yes, it's a common variant.

Is it published anywhere? It is not among the ten proofs given in The

Book of Prime Number Records.

May 8, 2005, 9:21:39â€¯AM5/8/05

to

Norman Megill <n...@see.signature> writes:

> I used Euclid's proof from _The Book of Prime Number Records_, which

> starts off: "Suppose that p_1 = 2 < p_2 = 3 < ... < p_r are all the

> primes."

This assumption, which is completely pointless, does not occur in

Euclid's original proof. See

http://aleph0.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html

> Is it published anywhere?

I believe it's a pretty common variant among published proofs.

May 8, 2005, 10:46:20â€¯AM5/8/05

to

Norman Megill wrote:

>

> For any natural number n, the smallest divisor (greater than 1) of

n!+1

> is a prime greater than n. Hence there is no largest prime.

>

>

> For any natural number n, the smallest divisor (greater than 1) of

n!+1

> is a prime greater than n. Hence there is no largest prime.

>

That's cool!

But doesn't the proposition "the smallest divisor (greater than 1)

of n!+1 is a prime greater than n" itself require proof?

For example:

suppose not. then

1. suppose n itself is a factor of n! + 1. But it is also a

factor of n!. Therefore it has to be a factor of 1, which is absurd.

2. suppose one of the n-1, n-2, etc. is a factor. It is also a

factor of n!, etc.

These proofs BTW are similar to how Euclid proves that a*b*c+1 is

either prime or has a prime factor different from a, b, c, where a,

b, c are arbitrary primes, specifically the latter.

Thanks.

Ken

May 8, 2005, 11:30:56â€¯AM5/8/05

to

On 8 May 2005 07:46:20 -0700, "ken quirici" <kqui...@yahoo.com>

wrote:

wrote:

>Norman Megill wrote:

>>

>> For any natural number n, the smallest divisor (greater than 1) of

>n!+1

>> is a prime greater than n. Hence there is no largest prime.

>>

>

>That's cool!

>

>But doesn't the proposition "the smallest divisor (greater than 1)

>of n!+1 is a prime greater than n" itself require proof?

The proof is trivial. Say d is the smallest divisor of n! with d > 1.

Then d is prime, because if d is not prime then there exists d'

with 1 < d' < d and such that d' is a divisor of d, and it follows

that d' is also a divisor of n! + 1, contradicting the choice of

d. Also d > n, because no number < n is a divisor of n! + 1

(because if 1 < m <= n then the remainder on dividing n! + 1

by m is 1.)

>For example:

>

>suppose not. then

> 1. suppose n itself is a factor of n! + 1. But it is also a

>factor of n!. Therefore it has to be a factor of 1, which is absurd.

>

> 2. suppose one of the n-1, n-2, etc. is a factor. It is also a

>factor of n!, etc.

>

>These proofs BTW are similar to how Euclid proves that a*b*c+1 is

>either prime or has a prime factor different from a, b, c, where a,

>b, c are arbitrary primes, specifically the latter.

>

>Thanks.

>

>Ken

************************

David C. Ullrich

May 8, 2005, 12:10:23â€¯PM5/8/05

to

ken quirici wrote:

> But doesn't the proposition "the smallest divisor (greater than 1)

> of n!+1 is a prime greater than n" itself require proof?

Here is a very explicit version of the entire proof:

Suppose there are a finite number of primes. Let p be the largest. Let

q be the smallest divisor (greater than 1) of p!+1. (The set of

divisors of p!+1 is nonempty, since p!+1 is one of them, and by the

well-ordering principle there is a smallest, which we will call q.) Then

none of 2,3,4,...,p divides q since otherwise it would also divide

p!+1, which is impossible. (2,3,4,...,p all divide p!, so none divides

p!+1.) And none of p+1,...,q-1 divides q since otherwise it would also

divide p!+1, and then q would not be the smallest divisor of p!+1.

Therefore q is prime, and q > p, so p is not the largest prime.

May 8, 2005, 12:25:36â€¯PM5/8/05

to

BTW if you _really_ want explicit detail, the computer-verified metamath

versions are found here:

versions are found here:

http://us2.metamath.org:8888/mpegif/infpnlem1.html - The smallest

divisor (greater than 1) q of p! + 1 is a prime greater than p.

http://us2.metamath.org:8888/mpegif/infpnlem2.html - Therefore for any

natural number p, there exists a prime greater than p.

http://us2.metamath.org:8888/mpegif/infpn.html - Therefore the set of

all primes is equinumerous to the set of natural numbers, i.e. is

infinite.

May 8, 2005, 2:55:55â€¯PM5/8/05

to

Wow. I took a look at these. I had no idea a formal proof required such

if you'll pardon the expression excruciating precision.

Thanks.

Ken

May 8, 2005, 4:24:32â€¯PM5/8/05

to

Norman Megill wrote:

> Torkel Franzen wrote:

>

> > Norman Megill <n...@see.signature> writes:

> >

> >>(Specifically, this proof

> >>avoids the product of a hypothetical finite set of all primes,

which I

> >>found cumbersome to work with.)

> >

> > There is no such set in Euclid's proof.

>

> I used Euclid's proof from _The Book of Prime Number Records_, which

> starts off: "Suppose that p_1 = 2 < p_2 = 3 < ... < p_r are all the

> primes." This specifies a function from {1,...,r} onto a

hypothetized

> finite set of all primes. Whether this is what Euclid intended is

> another matter - set theory not having been invented yet. :) My goal

> was simply to formalize it under modern set theory.

>

> Torkel Franzen wrote:

>

> > Norman Megill <n...@see.signature> writes:

> >

> >>(Specifically, this proof

> >>avoids the product of a hypothetical finite set of all primes,

which I

> >>found cumbersome to work with.)

> >

> > There is no such set in Euclid's proof.

>

> I used Euclid's proof from _The Book of Prime Number Records_, which

> starts off: "Suppose that p_1 = 2 < p_2 = 3 < ... < p_r are all the

> primes." This specifies a function from {1,...,r} onto a

hypothetized

> finite set of all primes. Whether this is what Euclid intended is

> another matter - set theory not having been invented yet. :) My goal

> was simply to formalize it under modern set theory.

>

I'm not sure why this is so difficult to formalize. You don't need the

fact that the finite set is ordered, for instance. Are you allowed

abbreviations in your system? Using ZF axioms you would, as you say,

consider the wff that there exists a one-to-one onto function from

{1,...,n} to P. If you are allowed abbreviations, then abbreviate this

wff as Mn,P ("the size of P is n"). You should be proving things about

Mn,P in any case, since they are of fundamental interest. Once you

have these then the standard proof goes through - in my eyes, in a

simpler form, since it does not require the definition of the factorial

function. The crucial theorem (VI1.56 in my system) is "For every

finite set of natural numbers, there exists a non-zero number which

they all divide." This can be proved by induction on the size of the

finite set.

May 8, 2005, 5:26:23â€¯PM5/8/05

to

May 8, 2005, 6:03:06â€¯PM5/8/05

to

Helene....@wanadoo.fr wrote:

> Helene.Bouc...@wanadoo.fr wrote:

>>function. The crucial theorem (VI1.56 in my system) is "For every

> Helene.Bouc...@wanadoo.fr wrote:

>>function. The crucial theorem (VI1.56 in my system) is "For every

I am not familiar with your system. Can you provide a reference?

>>finite set of natural numbers, there exists a non-zero number which

>>they all divide."

>

> Sorry, this should be "For every finite set of non-zero natural

> numbers, there exists a non-zero number which they all divide."

BTW in my system I already had the factorial function available, since

it is used for other things. That might make a difference. I will

look at your system and consider your remarks. Thanks.

May 9, 2005, 1:13:10â€¯AM5/9/05

to

Norman Megill wrote:

> Helene....@wanadoo.fr wrote:

> > Helene.Bouc...@wanadoo.fr wrote:

> >>function. The crucial theorem (VI1.56 in my system) is "For every

>

> I am not familiar with your system. Can you provide a reference?

http://www.andrewboucher.com/papers/foea/index.htm

Section VI Chapter 1 contains the theorem referenced above.

Section VII Chapter 4 contains the proof of the infinitude of primes.

>

> >>finite set of natural numbers, there exists a non-zero number which

> >>they all divide."

> >

> > Sorry, this should be "For every finite set of non-zero natural

> > numbers, there exists a non-zero number which they all divide."

>

> BTW in my system I already had the factorial function available,

since

> it is used for other things. That might make a difference. I will

> look at your system and consider your remarks. Thanks.

I think that's it, actually. If you already have the factorial and

have proved properties about the factorial, then your proof is probably

simpler, in the sense of being shortest. There may of course be other

measures of simplicity, as you undoubtedly realize (after so much

work!), such as (say) the number of concepts/definitions required, the

nesting used, etc., not to mention just some intuitive idea of

"simplicity." After a night's sleep, I kinda like your proof, given

you already have the factorial available.

May 9, 2005, 4:00:44â€¯AM5/9/05

to

Norman Megill wrote:

> Here is the proof:

>

> For any natural number n, the smallest divisor (greater than 1) of n!+1

> is a prime greater than n. Hence there is no largest prime.

>

> As simple as it is, I was unable to find a published reference for this

> proof. Is it a known proof?

I've used this in my lectures many times :-)

--

Robin Chapman, www.maths.ex.ac.uk/~rjc/rjc.html

"Elegance is an algorithm"

Iain M. Banks, _The Algebraist_

May 9, 2005, 11:26:20â€¯PM5/9/05

to

Helene....@wanadoo.fr wrote:

>

> http://www.andrewboucher.com/papers/foea/index.htm

>

> Section VI Chapter 1 contains the theorem referenced above.

> Section VII Chapter 4 contains the proof of the infinitude of primes.

>

>

> http://www.andrewboucher.com/papers/foea/index.htm

>

> Section VI Chapter 1 contains the theorem referenced above.

> Section VII Chapter 4 contains the proof of the infinitude of primes.

>

That is an impressive piece of work, very nice. I'll keep it on file

for reference. Did you use any software to check the accuracy of the

proofs?

May 10, 2005, 1:15:09â€¯AM5/10/05

to

Norman Megill wrote:

> Helene....@wanadoo.fr wrote:

> >

> > http://www.andrewboucher.com/papers/foea/index.htm

> >

> > Section VI Chapter 1 contains the theorem referenced above.

> > Section VII Chapter 4 contains the proof of the infinitude of

primes.

> >

>

> That is an impressive piece of work, very nice. I'll keep it on file

> for reference.

Thank you.

> Did you use any software to check the accuracy of the

> proofs?

>

No it's all manually done.

May 10, 2005, 12:03:15â€¯PM5/10/05

to

. (Specifically, this proof

avoids the product of a hypothetical finite set of all primes, which I

found cumbersome to work with.)

Torkel Franzen wrote:

There is no such set in Euclid's proof.

Yes, there is. Here is the original Euclid.

text:

"Let A, B, C the assigned prime numbers.

I say that there is more primes than those assigned."

Take the least number DE measured by A, B, and C

add the unit DF to DE ...."

Clearly, the 'assigned number of primes' are the finite

set of all numbers accepted as primes.

'The least number mesured by' is the product of them.

Ludovicus

May 10, 2005, 12:17:07â€¯PM5/10/05

to

lui...@yahoo.com writes:

> Clearly, the 'assigned number of primes' are the finite

> set of all numbers accepted as primes.

"Accepted as primes" means nothing. Do you have the idea that

Euclid is assuming that A,B,C are all the primes? Not in the

translation I read. And since the assumption is perfectly

pointless, and isn't used in the proof, there is little

reason to think that Euclid made it.

May 10, 2005, 12:26:47â€¯PM5/10/05

to

lui...@yahoo.com wrote:

> . (Specifically, this proof

> avoids the product of a hypothetical finite set of all primes, which I

> found cumbersome to work with.)

> Torkel Franzen wrote:

> There is no such set in Euclid's proof.

> Yes, there is. Here is the original Euclid.

> text:

> "Let A, B, C the assigned prime numbers.

> I say that there is more primes than those assigned."

> Take the least number DE measured by A, B, and C

> add the unit DF to DE ...."

> . (Specifically, this proof

> avoids the product of a hypothetical finite set of all primes, which I

> found cumbersome to work with.)

> Torkel Franzen wrote:

> There is no such set in Euclid's proof.

> Yes, there is. Here is the original Euclid.

> text:

> "Let A, B, C the assigned prime numbers.

> I say that there is more primes than those assigned."

> Take the least number DE measured by A, B, and C

> add the unit DF to DE ...."

Euclid wrote in broken English? I never knew that.

> Clearly, the 'assigned number of primes' are the finite

> set of all numbers accepted as primes.

Actually, I thought that 'the assigned prime numbers'

was clearly an arbitrary finite set of primes, and the proof

showed that whatever finite set of primes you picked

it could not be the set of all primes.

May 10, 2005, 2:15:22â€¯PM5/10/05

to

> . (Specifically, this proof

> avoids the product of a hypothetical finite set of all primes, which I

> found cumbersome to work with.)

>

> Torkel Franzen wrote:

>

> There is no such set in Euclid's proof.

>

> Yes, there is. Here is the original Euclid.

> text:

> "Let A, B, C the assigned prime numbers.

> I say that there is more primes than those assigned."

> Take the least number DE measured by A, B, and C

> add the unit DF to DE ...."

>

> Clearly, the 'assigned number of primes' are the finite

> set of all numbers accepted as primes.

No. Read the statement of the proposition. Something like this...

Given any list of primes, to find a prime not in the list.

This could be a useful construction even if you do not

assume there are finitely many primes.

--

G. A. Edgar http://www.math.ohio-state.edu/~edgar/

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu