Vestrucci, AndreaAndreaVestrucci0000-0002-6336-10362026-10-052026-10-0520261432-06650933-5846https://fis.uni-bamberg.de/handle/uniba/117549We present a type-disciplined, compositional reconstruction of the diagonal strategy in Gödel’s first incompleteness theorem. The goal is not a new or “more direct” proof of incompleteness, but an explicit computational unpacking of the mechanism. The paper exhibits a concrete pipeline of code-transformers between primitive recursive syntactic domains, thereby avoiding well-definedness issues arising in Lindenbaum-quotient formulations. A central feature is the separation between a graph-mediated witness form of the Gödel sentence and a canonical normal form, connected by an internal normalization lemma formalizable in the base theory. The paper also presents the construction categorically in a category of primitive recursive code domains and morphisms, and extracts a general diagonal-flipping blueprint clarifying how type stratification distinguishes paradoxical from limitative diagonal arguments.engGödel’s first incompleteness theoremDiagonalizationGödel numberingPrimitive recursive functionsLawvere fixed-point theoremDiagonal argumentsarticle10.1007/s00153-026-01021-7