Martin Escardo 2012. \begin{code} {-# OPTIONS --without-K #-} module WLPO where open import GenericConvergentSequence open import CurryHoward open import Equality WLPO : Prp WLPO = ∀(u : ℕ∞) → u ≡ ∞ ∨ u ≢ ∞ \end{code} Navigate to the module GenericConvergentSequence for the definition of the type ℕ∞ and its role. More discussion is included in the module TheTopologyOfTheUniverse. The weak principle of omniscience WLPO is independent of type theory: it holds in the model of classical sets, and it fails in recursive models, because it amounts to a solution of the Halting Problem. But we want to keep it undecided, for the sake of being compatible with classical mathematics, following the wishes of Bishop, and perhaps upsetting those of Brouwer who was happy to accept continuity principles that falsify WLPO. In the words of Aczel, WLPO is a taboo. More generally, anything that implies a taboo is a taboo, and any taboo is undecided. Taboos are boundary propositions: they are classically true, recursively false, and constructively, well, taboos!