On Revisiting Gödel's Incompleteness and Turing's Undecidability of the Halting Problem

This version is superseded, The only active version for now is V.10.0 Abstract : This paper re-examines the diagonal constructions that stand behind Gödel incompleteness, the undecidability of the halting problem, and Tarski undefinability of truth. Sections 1–8 fix the working apparatus: recursive functions, arithmetization, Turing machines, Kleene’s normal form, the language and axioms of PA, Gödel numbering of L_PA, and the representability of primitive recursive relations, including an exponentiation relation defined by register sums. Section 9 treats the diagonal step. Some presentations (the Stanford Encyclopedia’s two supplements on incompleteness, Nagel and Newman’s account of Sub) move between a number, a numeral string, and a code without fixing the map. The mixed expression Sub(p, ⌜x⌝, p̄) is ill-typed; the two coherent maps compute different values. A form of the diagonal lemma that uses a representing formula Number_PA is a theorem about numbers. Questions about sentences and individuals are deferred to Section 10.1. PA proves equalities between distinct terms for the same number; coding tracks strings. D1 and D2 lift G ↔ K to the two codes of prov_PA. A formula that records both a canonical code and an additive code and attaches the fixed point to one code yields a fork: face-value Σ₁-unsoundness, refused because ℕ satisfies PA, or a provability predicate that does not track independently of the term. The step PA ⊬ G ⇒ ℕ ⊨ ¬prov(⌜G⌝) is then unavailable. A parameterized form of Hilbert–Bernays D1, with a Δ₀ fixed point A(k), is used in an argument that ZF as a meta-theory for PA proves ⊥ if that formula is treated as well-defined. The resources that make Form_PA a set and ⌜·⌝ total are stated; they license p = ⌜φ⌝ and do not keep a numerical quantifier independent of a syntactic domain. At that p, with ψ ≡ ¬prov_PA, Kleene’s normal form writes unprovability as a claim about traces. Separation cannot form E = {x ∈ ℕ | φ(x)}. The same inversion is applied to D(x) = 1 − H(x,x) and to the Liar. Under Turing’s totality assumption, H(x,x) = 1 iff Halt(x,x), and there is no index for that specification. A corollary records Π₁-completeness for true primitive recursive universal sentences, given a lift of the output-1 clause from ℕ into PA. Section 10 reads compactness for a non-standard model, Cantor’s argument, and the Löwenheim–Skolem theorem as results about a meta-theory that already contains completed ω and impredicative Separation. Löwenheim–Skolem is a constraint on definability: a countable language supplies countably many formulas and existentials satisfied by one witness each. The internal/external distinction describes satisfaction in a model; it does not answer what ZF can define. Uncountability as a completed collection commits to sets that L_ZF does not name. ZF does not define uncountable structure in an absolute sense. Section 11 traces the historical choice between incomplete symbols and completed totalities. The limitative theorems are constructions whose inverting instances are not well-defined predicates. They are not boundaries of thought. They are symptoms of forcing Aristotelian logic to reason about Platonic objects. Description : This paper re-examines the diagonal constructions behind Gödel incompleteness, the undecidability of the halting problem, and Tarski undefinability of truth. Sections 1–8 set out the working apparatus: recursive functions, arithmetization, Turing machines, Kleene’s normal form, Peano arithmetic, Gödel numbering of L_PA, and representability of primitive recursive relations. Exponentiation inside PA is defined as a relation by register sums, used to decode prime-power codes. Section 9 is the technical core. Numerals, numbers, and codes are kept distinct. Standard presentations of substitution (SEP supplements; Nagel–Newman) are separated into two typed maps; the mixed expression Sub(p, ⌜x⌝, p̄) is ill-typed. A form of the diagonal lemma that uses Number_PA is a theorem about numbers. PA proves equalities between distinct terms for the same number; coding tracks strings. D1 and D2 lift G ↔ K to the codes of prov_PA. A formula that records both a canonical code and an additive code and attaches the fixed point to one code yields a fork: face-value Σ₁-unsoundness, refused because ℕ ⊨ PA, or a provability predicate that does not track independently of the term. The informal step PA ⊬ G ⇒ ℕ ⊨ ¬prov(⌜G⌝) is then unavailable. A parameterized form of Hilbert–Bernays D1, with a Δ₀ fixed point A(k), is used in an argument that ZF as a meta-theory for PA proves ⊥ if that formula is treated as well-defined. Con(PA) is the L_ZF-sentence that formalizes PA ⊬ ⊥ (Hilbert–Bernays); that ω ⊨ PA is cited from Kunen. The resources that make Form_PA a set and ⌜·⌝ total are stated; they license p = ⌜φ⌝ and do not keep a numerical quantifier independent of a syntactic domain. At that p, Kleene’s normal form writes unprovability as a claim about traces. Separation cannot form E = {x ∈ ℕ | φ(x)}. The same inversion is applied to D(x) = 1 − H(x,x) and to the Liar. Under Turing’s totality assumption there is no index for that specification. A corollary records Π₁-completeness for true sentences with a primitive recursive matrix. Section 10 treats compactness for a non-standard model, Cantor’s argument, and Löwenheim–Skolem as results about a meta-theory that already contains completed ω and impredicative Separation. Löwenheim–Skolem is read as a constraint on definability, not as a paradox dissolved by an internal/external label. Uncountability as a completed collection commits to sets that L_ZF does not name. ZF does not define uncountable structure in an absolute sense. Section 11 is historical and ontological: Plato and Aristotle, Frege, Russell and Whitehead, the choice of ZF, and Banach–Tarski. This is a self-contained preprint (source and PDF). It constructs the classical framework before criticizing the diagonal step. It is offered for community scrutiny. I do not claim a machine-checked formalization. Comments and objections are welcome, including on particular subsections of Section 9 (typing of Sub, the lift of G ↔ K, the Δ₀ fixed point, the extension check, or the halting application). Write to marwanezerradi2@gmail.com. Please cite the version number on this record. Important note: This is Version 9.0 (September 2026). All previous Zenodo versions (February–June 2026 and Versions 7–8, September 2026) are superseded. They should not be cited. Contact: marwanezerradi2@gmail.com Version history• V.9.0 (September 2026): Section 9.1 shortened and confined to maps; sentences and individuals deferred to 10.1. D1–D2 lift of G ↔ K added in 9.2. Divergent fixed point rewritten: Σ₁-unsoundness refused because ℕ ⊨ PA; the same fork stated for prov on ℕ; the Gödel step PA ⊬ G ⇒ ℕ ⊨ ¬prov(⌜G⌝) marked as unavailable. Inconsistency argument for ZF as meta-theory aligned with Con(PA) as an L_ZF-sentence (Hilbert–Bernays, Kunen). Halting paragraph records totality of H and the absence of an index for D. Cantor and Löwenheim–Skolem rewritten (impredicative Separation; definability; internal/external as bookkeeping). Neutral-meta-theory programme removed. Abstract, introduction, and conclusion aligned with the body.• V.8.0 (September 2026): Revised abstract and introduction; typed substitution and Number_PA form of the diagonal lemma; divergent fixed point; parameterized D1 and ZF_ω; extension collapse via Kleene; halting specification and the Liar; Π₁-completeness; meta-theory and ontology sections; Hilbert–Bernays and Kunen for model-theoretic consistency of PA.