natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
The theory of objects is the logical theory whose models in a category $\mathcal{C}$ are precisely the objects of $\mathcal{C}$.
The theory of objects $O$ is the theory with no axioms over the signature with a single type and no primitive symbols except equality.
Of course, $O$ is a geometric theory, and as models for $O$ in a topos $\mathcal{E}$ correspond to objects of $\mathcal{E}$, we can use its classifying topos to get a representation of the objects of $\mathcal{E}$.
The classifying topos for the theory of objects is the presheaf topos $[FinSet, Set]$ over the opposite category of the category FinSet of finite sets.
See at classifying topos for the theory of objects.
For more general base toposes $\mathcal{S}$, it is a theorem due to Andreas Blass that the theory of objects has a classifying topos precisely if $\mathcal{S}$ has a natural numbers object.
Closely related to $O$ is the theory of pointed objects $O_\ast$ which is the empty theory over a signature with of a single constant. Its models are pointed objects and its classifying topos is $[FinSet_\ast,Set]$. (See the discussion&references at classifying topos for the theory of objects.)
The next step up on the ladder of logical complexity is the theory of inhabited objects $O_\exists$ that adds to $O$ the existential axiom $\top\vdash(\exists x)\top$. Its classifying topos $Set[O_\exists]$ is the functor category $[FinSet_\exists, Set]$ with $FinSet_\exists$ the category of finite nonempty sets. It has the property that every topos $\mathcal{E}$ admits a localic morphism to $Set[O_\exists]$.^{1}
Sections B4.2, D3.2 of
cf. Johnstone (2002 II, p.773) and Joyal-Tierney (1984). For some further information on $FinSet_\exists$ see the references at generic interval. ↩
Last revised on August 5, 2014 at 04:39:24. See the history of this page for a list of all contributions to it.