The Cut-Elimination System CERES

The Prime Proof

On this page you can find supplementing material to our paper: "CERES: An analysis of Fürstenberg's proof of the infinity of primes".

In this paper we use the system CERES to analyze Fürstenberg's topological proof of the infinity of primes. Showing that Euclid's original proof can be obtained as one of the analytic arguments from Fürstenberg's proof.

This analysis is based on the characteristic clause sets of the schematic proof-formalization of Fürstenberg's topological proof. The characteristic clause sets of selected cases are given below. Note that, these are redundancy-free in terms of tautology elimination and subsumption.

One aspect in which the application of CERES on this example differs from the other examples is in the method of refutation of the characteristic clause sets. We have failed, after a systematic application of the theorem provers Prover9 and Otter, to produce a refutation in a fully automatic manner. Therefore, we have refuted the sets using our interactive resolution theorem prover ATP. A technical report describing the refutation of the set for the three primes proof can be found here.

The formalization of Fürstenberg's proof is divided into the following parts:

defs.hlk - basic definitions and axioms,
c_union.hlk - proves that the union of two closed sets is again closed,
inf_proof.hlk - proves that all open non-empty sets are infinite,
prog_closed.hlk - proves that progressions are closed,
main.hlk - schematic version of Fürstenberg's topological proof.

You need to have all these files together with the concrete instantiation files (which you will find further below) in order to successfully run the HLK compiler on them.

Note that, due to their sizes, some of the following files are compressed (gziped). We recommend you leave them compressed since uncompressing would yield files of tremendous sizes (more then 1 GB in some cases). Besides the system CERES and all our tools are also capable of working with gziped files directly.

These are some exemplary cases assuming only k + 1 primes exist.

instance of the above proof scheme assuming only one prime exists (k = 0):

$ hlk --ceres -o prime0.xml prime0.hlk the-proof

$ ceres -sk -cs prime0.xml the-proof prime0-ce.xml

Supplemental files: prime0-ce.pdf (characteristic clause set and axioms)
instance of the above proof scheme assuming only two primes exist (k = 1):

$ hlk --ceres -o prime1.xml prime1.hlk the-proof

$ ceres -sk -cs prime1.xml the-proof prime1-ce.xml

Supplemental files: prime1-ce.pdf (characteristic clause set and axioms)
instance of the above proof scheme assuming only three primes exist (k = 2):

$ hlk --ceres -o prime2.xml prime2.hlk the-proof

$ ceres -sk -cs prime2.xml the-proof prime2-ce.xml

Supplemental files: prime2-ce.pdf (characteristic clause set and axioms)
instance of the above proof scheme assuming only four primes exist (k = 3):

$ hlk --ceres -o prime3.xml prime3.hlk the-proof

$ ceres -sk -cs prime3.xml the-proof prime3-ce.xml

Supplemental files: prime3-ce.pdf (characteristic clause set and axioms)
instance of the above proof scheme assuming only thirteen primes exist (k = 12):

$ hlk --ceres -o prime12.xml prime12.hlk the-proof

$ ceres -sk -cs prime12.xml the-proof prime12-ce.xml

Supplemental files: prime12-ce.pdf (characteristic clause set and axioms)