nLab introspective theory

Idea

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.

Definition

There are two useful equivalent definitions of introspective theory.

Definition

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)$.

Definition

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}(-))$:

Related Concepts

• Löb’s theorem

• incompleteness theorem

References

• Sridhar Ramesh, Introspective Theories and Geminal Categories, PhD thesis, Berkeley (2023) [escholarship:3mn0c475, pdf]