Martin Escardo 2012.


{-# OPTIONS --without-K #-}

module WLPO where

open import GenericConvergentSequence
open import CurryHoward
open import Equality

WLPO : Prp
WLPO = ∀(u : ℕ∞)  u    u  


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!