[[!redirects decidable existential quantifiers]] ## Contents ## * table of contents {:toc} ## Definition ## Given a [[decidable setoid]] $T$, a **decidable existential quantifier on $T$** is a function $\exists x.(-)(x):(T \to \mathbb{2}) \to \mathbb{2}$ with a term $$p:\prod_{P:T \to \mathbb{2}} \left(\prod_{t:T} P(t) = 0\right) \to (\exists x.P(x) \equiv 0) \times \left(\left(\prod_{t:T} P(t) = 0\right) \to \emptyset \right) \to (\exists x.P(x) \equiv 1)$$ ## See also ## * [[booleans]] * [[decidable setoid]] * [[decidable universal quantifier]] category: not redirected to nlab yet