An Intuitionistic Glance at Primes

This paper gives a proof-theoretic account of how positive integers must be classified as $1$, prime, or composite in intuitionistic logic.

Compositehood is expressed in $\Sigma^0_0$ by exhibiting a factorization; primality is expressed in $\Pi^0_0$ by exhibiting a lack of interior factorization.

Because both searches are bounded, both predicates are decidable.

Organizing the checks in stages yields a recursive sieve for the primes, a characterization of modular cancellation, and finite arithmetic certificates.

The final sections distinguish what Heyting Arithmetic ($\mathsf{HA}$) proves internally from what depends on the standard interpretation of $\mathbb{N}$.