**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 IntegerThe 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 ShowThe 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 kWe 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 neverSo 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

`Or`red together:

> subproperties (Or ps) = ps > subproperties p = [p]Now we can go ahead and remove all of the

`And`s:

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

`always`can be rewritten as:

> removeAnd (And []) = Modulo 0 1Remove

`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 = pBy 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

`And`s, and so must simply be the

`Or`of a bunch of

`Modulo`s. 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`.

Connection between logic and topology is discussed in that nice paper: http://lambda-the-ultimate.org/node/4037

ReplyDelete(Maybe you already know about it)

@polus Yes, I know that paper, though I haven't read all of it. I love the connection between computation and topology. I think it's really profound and it should be better known. These days, any time I see some point set topology, my first question is "how does this relate to computation?".

ReplyDelete@sigfpe I'm curious about your perception that the connection between topology and computation is "profound".

ReplyDeleteMy own feeling is that, depending on your mathematical ontology, the connection is either just a "pun", or an identity, i.e. that topology is computation seen through a glass darkly.

The thing that links them is fuzzy membership "along the edges". In computation, this is a direct consequence of the halting problem; in topology because of the limitation to a finite number of intersections.

If you believe that mathematical objects "exist" independent of computations, then I would say this is a "pun". If you believe, as I do, that only mathematical objects that can be computed (perhaps for a slightly extended notion of "computed") exist, then the two notions are identical, and we just have two formalisms for the same phenomenon (useful perhaps, but not profound).

Or perhaps, we just find different things "profound". ;-)

@Marc Interesting.

ReplyDeleteI went through my mathematical education studying courses in point-set topology, algebraic topology and homotopy theory and at no point did anyone point out to me that there was any connection to computation. When I finally came across it a few years back I was blown away. I find it amazing to see the same language that I'd used to describe the deformation of rubber sheets being used to talk about computation. A connection between two different areas of mathematics like this is an example of what I'd call "profound". That's what a large part of mathematics is about, finding ever deeper structures that are found in more and more places.

Along similar lines I'd say that the Curry-Howard isomorphism is also profound. It's another example of how the same language appear in two different places. In the case of Curry-Howard it's less profound, after all, a priori we expect many connections between logic and computing. But connecting rubber sheets and the discrete actions of machines is much more surprising.

@sigfpe

ReplyDeleteThanks for the thoughtful response!

It sounds like "profound" is a partial synonym with "surprising", and surprising is, of course, always a bit subjective.

I'm probably warped by the fact that I got into mathematics backwards: I went from computation to category theory, and only then started to learn set theory, topology, etc. I probably have an inverted sense of surprise in this regard. (I was more shocked when I discovered how much of mathematics goes on with no conscious consideration of computation. ;-) )

@Marc You can get an idea of how surprising this stuff is for mathematicians by the score I got here: http://mathoverflow.net/questions/19152/why-is-a-topology-made-up-of-open-sets

ReplyDeleteI'm convinced there's a pile of interesting stuff to be mined from this when applied to physics, connected to some of the things Andrej Bauer says here: http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/

@sigfpe Andrej has definitely been one of my "people to watch" for a while!

ReplyDelete