Diagonalization as computation: Gödel sentence construction and a type-disciplined blueprint

Abstract We 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.