## The Prime-Divisor Proof

The *Prime-Divisor Proof* is a proof of the fact that
from the least number principle, it follows that
*every number greater than 1 has a prime divisor*. This theorem
is inferred from two Lemmas:

- The least number principle implies the induction principle, and
- The induction principle implies that every number greater than 1 has a prime divisor.

As the prime-divisor proof is formalized in second-order logic, the
first-order CERES method does not suffice to analyze the proof. The
generalization of the CERES method to higher-order logic,
CERES^{ω}, suffices. It is implemented within the
Generic Architecture for Proofs framework.

The proof was formalized using HLK.
Using the CERES compiler, the HLK source can be compiled into a
higher-order LK proof in our XML format. The XML files can be displayed
using ProofTool. Using
CERES^{ω}, a characteristic clause set is extracted. The
characteristic clause set contains third-order material that is introduced
by the use of Skolem functions. The characteristic clause set is output,
together with additional information, in PDF format.

`$ hlk --ceres -o primediv.xml primediv.hlk the-proof`

The following commands are performed using the Generic Architecture for Proofs framework.

`$ scala -classpath cli-1.0-alpha-shell.jar`

`scala> import at.logic.cli.GAPScalaInteractiveShellLibrary._`

`scala> val proof = loadProofs("primediv.xml").first`

`scala> val proof_sk = lkTolksk(proof)`

`scala> val struct = extractStruct(proof_sk)`

`scala> val cl = structToLabelledClausesList(struct)`

`scala> writeLabelledSequentListLatex(cl, "primediv.tex")`

`scala> exit`

`$ pdflatex primediv.tex`

The result is the file primediv.pdf
which contains the characteristic clause set of the proof. An
ℛ_{al}-refutation of the characteristic clause set can be found
here.