The weak limited principle of omniscience

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-08-08.
Last modified on 2025-01-07.

module foundation.weak-limited-principle-of-omniscience where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.disjunction
open import foundation.negation
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.decidable-propositions
open import foundation-core.propositions
open import foundation-core.sets

Statement

The weak limited principle of omniscience (WLPO) asserts that for any sequence f : ℕ → bool either f n is true for all n : ℕ or it is not. In particular, it is a restricted form of the law of excluded middle.

prop-WLPO : Prop lzero
prop-WLPO =
  ∀' (ℕ → bool) (λ f → is-decidable-Prop (∀' ℕ (λ n → is-true-Prop (f n))))

WLPO : UU lzero
WLPO = type-Prop prop-WLPO

is-prop-WLPO : is-prop WLPO
is-prop-WLPO = is-prop-type-Prop prop-WLPO

See also

Recent changes