Abstract:

This article assembles a detailed paper-level dependency chain for Gödel’s First and Second Incompleteness Theorems while identifying the effectiveness, consistency, and base-theory assumptions used at each stage. It separates computable enumerability from primitive-recursive axiomatizability; develops Gödel-style prime-power coding; fixes an explicit Hilbert calculus; gives capture-avoiding substitution with separate primitive-recursive majorants depending on all relevant variable indices; and proves primitive recursiveness of witness-annotated proof verification for a merely computably enumerable axiom set. The syntactic \( \Delta_0 \) and \( \Sigma_1 \) classes are fixed effectively, making the induction axioms of \( I\Sigma_1 \) primitive-recursively recognizable. The representability theorem is proved in \( Q \) by structural induction, using a finite-unfolding lemma, explicit \( \Sigma_1 \) closure under composition, and a displayed witness history for primitive recursion. For provability theory, the article defines a canonical trace-based proof predicate and gives detailed construction schemas, with explicit \( \Sigma_1 \)-induction invariants, for proof transformations and bounded proof synthesis in \( I\Sigma_1 \). These yield formalized \( \Sigma_1 \)-completeness, the Hilbert–Bernays–Löb derivability conditions, Löb’s theorem, and the Second Incompleteness Theorem. The article also proves Rosser’s strengthening, states Tarski’s theorem as the nondefinability of \( \mathrm{Th}(\mathbb{N}) \) in arithmetic, and marks the limits of anti-mechanist interpretations. Its contribution is expository and organizational rather than a new incompleteness theorem.