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

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:

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.