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 $D$ is the logical theory whose models in a coherent category are precisely the decidable objects.
The theory of decidable objects $D$is the theory 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_D(\mathcal{E})$ is the category of decidable objects in $\mathcal{E}$. The classifying topos $Set[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[D]$ is a locally decidable topos.
The theory of infinite decidable objects $D_\infty$ adds to $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 $D_\infty$ are precisely the infinite decidable objects and its classifying topos $Set[D_\infty]$ is the Schanuel topos.
Last revised on August 15, 2016 at 07:40:52. See the history of this page for a list of all contributions to it.