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:

• 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.