Gödel incompleteness through Arithmetic Universes after A. Joyal
arXiv:2004.10482
Abstract
We give proofs of Gödel's incompleteness theorems after A. Joyal. The proof uses internal category theory in an arithmetic universe, a predicative generalisation of topoi. Applications to Löb's Theorem are discussed.
31 pages, 4 figures