Gödel Incompleteness through Arithmetic Universes after A.~Joyal
Article
Formal Antecedent
Category Theory
Citation
Joost van Dijk and Alexander Gietelink Oldenziel. (2020). Gödel Incompleteness through Arithmetic Universes after A.~Joyal.
Why this reference is included
van Dijk and Oldenziel’s paper Gödel Incompleteness through Arithmetic Universes after A.~Joyal (2020) is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter The Self-Hosting Landscape; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “Examples: Altenkirch–Kaposi’s type theory in type theory (dependent type theory internalized in CIC with quotient inductive types ), Joyal’s arithmetic universes (internalize…”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Examples: Altenkirch–Kaposi's type theory in type theory (dependent type theory internalized in CIC with quotient inductive types ), Joyal's arithmetic universes (internalize enough to prove G\"odel's theorem internally ), Bocquet–Kaposi–Sattler's internal sconing (metatheorems via internal gluing )
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Joyal proposed arithmetic universes as a categorical framework that internalizes enough arithmetic to prove G\"odel's incompleteness theorem within the framework itself
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
1.3 @p1.2cmp3.0cmp3.0cmp2.3cm@ →prule Transition & Closest Precedent & Remaining Gap & τ Feature , E_0 → E_1 & Altenkirch–Kaposi 2016 ; Bocquet–Kaposi–Sattler 2023 & Non-Boolean, constructive adaptation to four-valued Ω_τ & Earned topos E_τ (I.D59) , E_1 → E_2 & Joyal arithmetic universes ; Abel graded modal DTT & Linear DTT not yet complete; no internal cut-elimination & 5 diagonal discipline; three-grade semiring , E_2 → E_3 & Willard 2001 (weak); Girard TX (fragments) & No full system at CIC-level proof-theoretic strength & *-autonomous proof theory via 5 (I.T39) , Book III pro
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
E_1 → E_2: Partially achieved. Internal proof-theoretic reasoning exists (Joyal arithmetic universes )
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Precedent (partial). No complete system achieving E_2 exists, but substantial partial results point the way: Joyal's arithmetic universes, analyzed by van Dijk and Gietelink Oldenziel , achieve internal incompleteness — the statement and proof of G\"odel's theorem inside a categorical framework