HLK ● ProofTool

TU Vienna ► logic.at ► Theory and Logic Group (E185-2)

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.

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)

© 2004-2010 Theory and Logic Group, Clemens Richter.