An Intuitionistic Glance at Primes

Abstract

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 $\hat{I}{\pounds }_0^0$ by exhibiting a factorization; primality is expressed in ${\hat{I}}_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}$.

42 pages, 4 figures. Corrigendum to v2: corrects the treatment of bounded factor search and separates decidable primality from oracle-strength completion principles

Topics & keywords