basic constructions: strong axioms further constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism In constructive mathematics, a set is exhaustible or omniscient if it satisfies a version of the limited principle of omniscience for the set rather than the natural numbers : the existential quantification of any decidable proposition on is again decidable. That is, or equivalently If you take the domain of discourse to be the...