The Infinitude of the Primes

Introduction

> import Data.List hiding (intersect)

A colleague at work reminded me of Fürstenberg's topological proof of the infinitude of primes. But as I tried to argue a while back, topology is really a kind of logic. So Fürstenberg's proof should unpack into a sort of logical proof. In fact, I'm going to unpack it into what I'll call the PLT proof of the infinitude of the primes. I apologise in advance that I'm just going to present the unpacked proof, and not how I got there from Fürstenberg's.

A small formal language
We're going to start with a little language. Propositions of this language are of type Prop:

> data Prop = Modulo Integer Integer

The intention is that Modulo k n is the property of an integer being equal to k modulo n. More precisely, it represents the property of being writable in the form sn+k for some s. (We disallow n=0.) But I also want to allow people to combine properties using "and" and "or". So we extend the language with:

>           | Or [Prop] | And [Prop] deriving Show

The intention now is that And ... holds when all of the properties in the list hold and similarly for Or .... We can write an interpreter to test whether integers have the specified property:

> eval (Modulo k n) x = (x-k) `mod` n == 0
> eval (Or ps)      x = or $ map (\p -> eval p x) ps
> eval (And ps)     x = and $ map (\p -> eval p x) ps

(Note we limit ourselves to *finite* compositions of And and Or, otherwise eval wouldn't actually define a property due to non-termination.

There are lots of things we can say in our language. For example we can give the 'extreme' properties that are never true or always true:

> never = Or []
> always = And []

We can say that one number is divisible by another:

> divisibleBy k = Modulo 0 k

We can test it with expressions like:

*Main> eval (divisibleBy 3) 9
True
*Main> eval (divisibleBy 5) 11
False

We can also express non-divisibility. We say that n isn't divisble by k by saying that n is either 1, 2, ..., or k-1 modulo k:

> notDivisibleBy n =
>     let n' = abs n
>     in Or (map (\i -> Modulo i n') [1..(n'-1)])

(Disallowing n=0.)

*Main> eval (notDivisibleBy 3) 9
False

Eliminating And
It's not obvious at first sight, but there is a big redundancy in our language. There is no need for And. Consider And [Modulo k1 n1, Modulo k2 n2]. This asserts, for the number x, that x = s*n1+k1 and x = t*n2+k2. The Chinese remainder theorem tells us that either these have no solution, or that this pair of propositions is equivalent to one of the form x = k3 mod n3 for some k3 and n3. So every time we And a pair of propositions we can eliminate the And by using the theorem. Solving for k3 and n3 is straightforward. I use the extended Euclidean algorithm and the proof of the Chinese remainder theorem given at Cut the Knot.

> egcd n1 n2 | n2 == 0 = (1, 0, n1)
>            | n1 == 0 = (0, 1, n2)
>            | otherwise = (y, x-y*(n1 `quot` n2), g)
>            where (x, y, g) = egcd n2 (n1 `mod` n2)

> intersect (Modulo k1 n1) (Modulo k2 n2) =
>     let (s, _, g) = egcd n1 n2
>         (q, r) = (k2-k1) `quotRem` g
>     in if r == 0
>         then Modulo (q*s*n1+k1) (n1*n2 `quot` g)
>         else never

So now we can repeatedly use intersect pairwise on our properties to eliminate all uses of And. Here is some code to do so. Firstly, it's convenient to sometimes write any property as if it is a list of "subproperties", all Orred together:

> subproperties (Or ps) = ps
> subproperties p = [p]

Now we can go ahead and remove all of the Ands:

> removeAnd (Or ps) = Or (map removeAnd ps)

The property always can be rewritten as:

> removeAnd (And []) = Modulo 0 1

Remove And from the head of the list, remove it from the tail of the list, and then form all possible intersections of these two parts:

> removeAnd (And (p:ps)) = Or [q `intersect` q' |
>     q <- subproperties (removeAnd p),
>     q' <- subproperties (removeAnd (And ps))]
> removeAnd p = p

By induction, the return value from removeAnd can no longer contain an And. Note that the properties can grow in size considerably. Here is the proposition that x isn't divisble by 5 or 7 written out in full:

*Main> removeAnd (And [notDivisibleBy 5, notDivisibleBy 7])
Or [Modulo 1 35,Modulo 16 35,Modulo 31 35,Modulo 46 35,Modulo 61
35,Modulo 76 35,Modulo (-13) 35,Modulo 2 35,Modulo 17 35,Modulo 32
35,Modulo 47 35,Modulo 62 35,Modulo (-27) 35,Modulo (-12) 35,Modulo
3 35,Modulo 18 35,Modulo 33 35,Modulo 48 35,Modulo (-41) 35,Modulo
(-26) 35,Modulo (-11) 35,Modulo 4 35,Modulo 19 35,Modulo 34 35]

Now to the primes. Here's a standard way to make the list of primes in Haskell:

> isPrime primes n = foldr (\p r -> p*p > n || (rem n p /= 0 && r))
>                          True primes
> primes = 2 : filter (isPrime primes) [3..]

The Proof
Now we can give the proof this set is infinite. Suppose it were finite. Then we could form this property:

> prop = removeAnd $ And (map notDivisibleBy primes)

It contains no Ands, and so must simply be the Or of a bunch of Modulos. But each Modulo defines an infinite set, so prop must define an infinite set.

But prop is the property of not being divisible by any prime. So prop can only eval to True on -1 or 1, a finite set. Contradiction. Therefore primes is infinite.

We can look at approximations to prop like this:

> prop' n = removeAnd $ And (map notDivisibleBy (take n primes))

You can see that the proposition grows in size rapidly:

*Main> removeAnd (prop' 3)
Or [Modulo 1 30,Modulo (-83) 30,Modulo (-167) 30,Modulo (-251)
30,Modulo 71 30,Modulo (-13) 30,Modulo (-97) 30,Modulo (-181) 30]
*Main> removeAnd (prop' 4)
Or [Modulo 1 210,Modulo (-56159) 210,Modulo (-112319) 210,Modulo...]

Nonetheless, it would always be finite if there were only finitely many primes. As primes is infinite, you can think of the sequence prop' n as somehow trying to creep up on the set -1, 1, never quite getting there.

Unfortunately I have no time to explain why a topological proof should lead to one about a simple DSL beyond mentioning that there's a deeper story relating to the computability of eval for possibly infinite expressions of type Prop.

Addendum
I'll just say a little on the computability connection. Suppose we have a really dumb algorithm to test whether an integer x equals k mod n by doing a brute force search for s such that x=s*n+k. Suppose this is the only kind of test on x that we have available to us. The test will only terminate if it finds a solution. So with such an algorithm, testing for equality mod N is only semi-decidable. Now suppose we are allowed multi-threaded code. The infinitude of the primes implies that with our dumb tests, membership of -1,1 is also semi-decidable. So we can turn the problem of proving the infinitude of the primes into one about computability. You can see roughly how: we can "semi-test" Or ps by launching a process to test the first element of ps. Then launch a process to check the next, and so on. If any of these processes terminates, we have our answer. The argument presented above gives the details of how to construct a suitable Or ps.