On the Realizability of Prime Conjectures in Heyting Arithmetic

TL;DR

This paper investigates the limitations of transforming primality concepts into explicit witnesses within Heyting Arithmetic, revealing fundamental constraints through geometric, proof-theoretic, and recursion-theoretic analyses.

Contribution

It introduces a novel multi-faceted approach to demonstrate the impossibility of uniform primality witness extraction in constructive logic.

Findings

No total functional can uniformly convert $ ext{Pi}_1$ primality into $ ext{Sigma}_1$ witnesses without normalization issues.

The geometric interpretation links primality to packing configurations, providing intuitive insight.

Recursion-theoretic analysis connects these constraints to the absence of total Skolem functions in PA.

Abstract

We show that no total functional can uniformly transform $\Pi_1$ primality into explicit $\Sigma_1$ witnesses without violating normalization in $\mathsf{HA}$. The argument proceeds through three complementary translations: a geometric interpretation in which compositeness and primality correspond to local and global packing configurations; a proof-theoretic analysis demonstrating the impossibility of uniform $\Sigma_1$ extraction; and a recursion-theoretic formulation linking these constraints to the absence of total Skolem functions in $\mathsf{PA}$. The formal analysis in constructive logic is followed by heuristic remarks interpreting the results in informational terms.