nLab
theory of decidable objects
Redirected from "theory of infinite decidable objects".
Contents
Context
Type theory
Topos Theory
topos theory
Background
Toposes
Internal Logic
Topos morphisms
Cohomology and homotopy
In higher category theory
Theorems
Contents
Idea
The theory of decidable objects is the logical theory 𝔻 \mathbb{D} whose models in a coherent category are precisely the decidable objects .
Definition
The theory of decidable objects is the theory 𝔻 \mathbb{D} over the signature with one sort and one binary relation ≠ \neq besides equality with axioms ( x ≠ x ) ⊢ x ⊥ (x \neq x)\vdash_x\perp and ⊤ ⊢ x , y ( ( x ≠ y ) ∨ ( x = y ) ) \top\vdash_{x,y} ((x \neq y)\vee(x=y)) .
Properties
For a topos ℰ \mathcal{E} the category of models Mod 𝔻 ( ℰ ) Mod_{\mathbb{D}}(\mathcal{E}) is the category of decidable objects in ℰ \mathcal{E} . The classifying topos Set [ 𝔻 ] Set[\mathbb{D}] for the theory of decidable objects is the functor category [ FinSet mono , Set ] [FinSet_{mono},Set] where FinSet mono FinSet_{mono} is the category of finite sets and monomorphisms. Set [ 𝔻 ] Set[\mathbb{D}] is a locally decidable topos .
Infinite decidable objects
The theory of infinite decidable objects 𝔻 ∞ \mathbb{D}_\infty adds to 𝔻 \mathbb{D} the axioms ⊤ ⊢ x 1 , … , x n ( ∃ y ) ⋀ i = 1 n ( y ≠ x i ) \top\vdash_{x_1,\dots,x_n} (\exists y)\bigwedge_{i=1}^{n}(y \neq x_i) for all n n with ⊤ ⊢ ( ∃ y ) ⊤ \top\vdash(\exists y)\top for n = 0 n=0 . The models of 𝔻 ∞ \mathbb{D}_\infty are precisely the infinite decidable objects and its classifying topos Set [ 𝔻 ∞ ] Set[\mathbb{D}_\infty] is the Schanuel topos .
References
Last revised on August 29, 2024 at 19:59:04.
See the history of this page for a list of all contributions to it.