A General Self-Reference Calculus: One Fixed-Point Theorem and One Diagonal Barrier Behind Gödel, Kleene, Löb, and NEMS Paper 26 of the NEMS Suite

We present a unified formal calculus of self-reference. From a single stratified interface separating semantic objects from syntactic codes, we prove one master fixed-point theorem and one master diagonal barrier, and recover Gödel's diagonal lemma, Kleene's recursion theorem, Löb-style self-reference, and the NEMS diagonal barrier as instances. The result is a machine-checked unification of major fixed-point and diagonal phenomena that are usually presented separately. The interface has two layers: a minimal layer (\SRIz) whose sole axiom is representability (repr-spec), and a re-entry extension (\SRIo) that additionally requires eval-quote. The Master Fixed-Point Theorem (\MFP-1) is the two-sorted mixed form p \simeq F(\ulcorner p\urcorner); the Master Diagonal Barrier (\MFP-2) rules out total deciders for nontrivial extensional predicates within the representable/internal class (not arbitrary external case-splitters). We prove a Semantic Diagonal Trichotomy via strict separation theorems across Strata 0/1/2, corresponding to NEMS Classes I, IIa, and IIb. Sharp minimality results show each axiom is necessary for its respective theorem—they are not ornamentation, but the precise rebuttal to the charge that the interface is over-engineered. The formalization lives in the SelfReference library of nems-lean; Section records Lean/Mathlib versions and distinguishes the direct NemS.Diagonal barrier route from optional abstract instance encodings (see the honesty note there on instance-route proof status). This overview isolates the calculus; stronger domain-specific and ontological packaging is deliberately left to adjacent papers. Trust boundary. Fixed-point and barrier theorems are conditional on the stratified SRI/CSRI interface and the explicit classical/constructive flags stated in the text; they unify diagonal phenomena in logic, not empirical physics by themselves. Machine-checked artifacts are cited as nems-lean . See .

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-09-13
DOI
https://doi.org/10.5281/zenodo.19429766
Primary Topic
Logic, programming, and type systems
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

A General Self-Reference Calculus: One Fixed-Point Theorem and One Diagonal Barrier Behind Gödel, Kleene, Löb, and NEMS Paper 26 of the NEMS Suite

Nova Spivack
Zenodo (CERN European Organization for Nuclear Research)
Logic, programming, and type systems
preprint

A General Self-Reference Calculus: One Fixed-Point Theorem and One Diagonal Barrier Behind Gödel, Kleene, Löb, and NEMS Paper 26 of the NEMS Suite

Nova Spivack
preprint en

Abstract

We present a unified formal calculus of self-reference. From a single stratified interface separating semantic objects from syntactic codes, we prove one master fixed-point theorem and one master diagonal barrier, and recover Gödel's diagonal lemma, Kleene's recursion theorem, Löb-style self-reference, and the NEMS diagonal barrier as instances. The result is a machine-checked unification of major fixed-point and diagonal phenomena that are usually presented separately. The interface has two layers: a minimal layer (\SRIz) whose sole axiom is representability (repr-spec), and a re-entry extension (\SRIo) that additionally requires eval-quote. The Master Fixed-Point Theorem (\MFP-1) is the two-sorted mixed form p \simeq F(\ulcorner p\urcorner); the Master Diagonal Barrier (\MFP-2) rules out total deciders for nontrivial extensional predicates within the representable/internal class (not arbitrary external case-splitters). We prove a Semantic Diagonal Trichotomy via strict separation theorems across Strata 0/1/2, corresponding to NEMS Classes I, IIa, and IIb. Sharp minimality results show each axiom is necessary for its respective theorem—they are not ornamentation, but the precise rebuttal to the charge that the interface is over-engineered. The formalization lives in the SelfReference library of nems-lean; Section records Lean/Mathlib versions and distinguishes the direct NemS.Diagonal barrier route from optional abstract instance encodings (see the honesty note there on instance-route proof status). This overview isolates the calculus; stronger domain-specific and ontological packaging is deliberately left to adjacent papers. Trust boundary. Fixed-point and barrier theorems are conditional on the stratified SRI/CSRI interface and the explicit classical/constructive flags stated in the text; they unify diagonal phenomena in logic, not empirical physics by themselves. Machine-checked artifacts are cited as nems-lean . See .

Zenodo (CERN European Organization for Nuclear Research)
Peace, Justice and strong institutions
Logic, programming, and type systems
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.