theory of decidable objects

**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 decidable objects* is the logical theory $\mathbb{D}$ whose models in a coherent category are precisely the decidable objects.

The *theory of decidable objects* is the theory $\mathbb{D}$ over the signature with one sort and one binary relation $#$ besides equality with axioms $(x#x)\vdash_x\perp$ and $\top\vdash_{x,y} ((x#y)\vee(x=y))$.

- For a topos $\mathcal{E}$ the category of models $Mod_{\mathbb{D}}(\mathcal{E})$ is the category of decidable objects in $\mathcal{E}$. The
*classifying topos*$Set[\mathbb{D}]$ for the theory of decidable objects is the functor category $[FinSet_{mono},Set]$ where $FinSet_{mono}$ is the category of finite sets and monomorphisms. $Set[\mathbb{D}]$ is a locally decidable topos.

- The theory of
*infinite decidable objects*$\mathbb{D}_\infty$ adds to $\mathbb{D}$ the axioms $\top\vdash_{x_1,\dots,x_n} (\exists y)\bigwedge_{i=1}^{n}(y#x_i)$ for all $n$ with $\top\vdash(\exists y)\top$ for $n=0$. The models of $\mathbb{D}_\infty$ are precisely the infinite decidable objects and its classifying topos $Set[\mathbb{D}_\infty]$ is the Schanuel topos.

- Peter Johnstone,
*Sketches of an Elephant II*, Oxford UP 2002. (pp.906,925)

Last revised on October 10, 2020 at 09:30:55. See the history of this page for a list of all contributions to it.