Proof-Theoretic Horizons: Approximability Without Reachability in Formal Theories

We isolate and formalize a proof-theoretic “horizon” phenomenon: a sentence defined asthe limit of a provable approximation scheme remains unprovable in a fixed theory T . Thenotion is theory-internal and relies only on standard arithmetization of syntax. Under thestandard hypotheses used for Gödel’s second incompleteness theorem (a weak arithmeticalbase plus a standard provability predicate satisfying the usual derivability conditions), weshow that every consistent, recursively axiomatized theory T admits a canonical horizonsentence. The result refines incompleteness in form by distinguishing mere unprovabilityfrom unreachability as a limit of provable approximants.