limited principle of omniscience
p
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The limited principle of omniscience () states that the existential quantification of any decidable proposition is again decidable. That is,
or equivalently
We have not stated the domain of quantification of the variable . If you take it to be the subsingleton corresponding to a given truth value and apply this principle to the.