Constructive taboos.
I think this terminology was coined by Peter Aczel.
Here is a list of typical constructive taboos.
* Excluded middle (EM). For every proposition P, either P holds or ¬ P holds.
* Weak excluded middle. For every proposition P, either ¬ P holds or ¬¬ P holds.
* De Morgan Law (DM). For all propositions P and Q, we have that ¬ (P and Q) ⇔ (¬ P or ¬ Q).
* Limited Principle of Omniscience (LPO). For every infinite binary sequence α, either there is n with αₙ ＝ 1, or else αₙ ＝ 0 for all n.
* Weak Limited Principle of Omniscience (WLPO). For every infinite binary sequence α, either αₙ = 1 for all n, or not.
* Lesser limited Principle of Omniscience (LLPO). For every infinite binary sequence with at most one 1, either the even terms are all 0, or the odd terms are all 0.
* The world's simplest axiom of choice (WSAC). Every family, all of whose elements are doubletons and which has at most one element, has a choice function.
1/
