An introspective theory is (very roughly) a category with an internal version of itself.
More specifically, an introspective theory is an essentially algebraic theory (a category with finite limits) such that every model of the theory itself contains a category with finite limits, with an internal model of the same theory, and with a homomorphism from the same model into (the global aspect of) the internal model.
It is a minimal abstract context in which Gödel incompleteness (more specifically, Löb’s theorem) arises. Introspective theories were introduced by Sridhar Ramesh in his 2023 thesis.
There are two useful equivalent definitions of introspective theory.
An introspective theory is
a category with finite limits $T$, with
an internal category with finite limits $C$ and
an indexed functor $F$ from the self-indexing $T/{-}$ to $C$ (viewed as a $T$-indexed category with finite limits):
The following definition is equivalent to the above, but it more directly resembles the concept described in the introduction. For $C$ an internal category in $T$, we below denote by $\mathrm{Hom}_T(1, C)$ the global aspect of $C$: the induced category with set of objects $\mathrm{Hom}_T(1, \mathrm{Ob}_C)$ and set of arrows $\mathrm{Hom}_T(1, \mathrm{Arr}_C)$.
An introspective theory is
a category with finite limits $T$, with
an internal category with finite limits $C$,
a finite limit preserving functor $\mathcal{S}$ from $T$ to $\mathrm{Hom}_T(1, C)$, and
a natural transformation $\mathcal{N}$ from the identity on $T$ to $\mathrm{Hom}_C(1, \mathcal{S}(-))$:
Last revised on October 7, 2024 at 09:18:15. See the history of this page for a list of all contributions to it.