The weak limited principle of omniscience
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Louis Wasserman.
Created on 2022-08-08.
Last modified on 2025-04-25.
module foundation.weak-limited-principle-of-omniscience where
Imports
open import elementary-number-theory.natural-numbers open import foundation.booleans open import foundation.coproduct-types open import foundation.decidable-subtypes open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-types open import foundation.equivalences open import foundation.limited-principle-of-omniscience open import foundation.logical-equivalences open import foundation.negation open import foundation.transport-along-identifications 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 open import logic.complements-decidable-subtypes
Statement
The weak limited principle of omniscience¶ (WLPO) asserts that every decidable subtype of the natural numbers is full or it is not. In particular, it is a restricted form of the law of excluded middle.
level-prop-WLPO : (l : Level) → Prop (lsuc l) level-prop-WLPO l = Π-Prop ( decidable-subtype l ℕ) ( λ P → is-decidable-Prop (is-full-decidable-subtype-Prop P)) level-WLPO : (l : Level) → UU (lsuc l) level-WLPO l = type-Prop (level-prop-WLPO l) WLPO : UUω WLPO = {l : Level} → level-WLPO l
Properties
The limited principle of omniscience implies the weak limited principle of omniscience
abstract level-WLPO-level-LPO : {l : Level} → level-LPO l → level-WLPO l level-WLPO-level-LPO lpo P = elim-disjunction ( is-decidable-Prop (is-full-decidable-subtype-Prop P)) ( λ (a , a∉P) → inr (λ full-P → ex-falso (a∉P (full-P a)))) ( λ ¬¬P → inl ( λ a → is-double-negation-stable-decidable-subtype ( P) ( a) ( λ a∉P → ¬¬P (a , a∉P)))) ( lpo (complement-decidable-subtype P))
Equivalent boolean formulation
bool-prop-WLPO : Prop lzero bool-prop-WLPO = ∀' (ℕ → bool) (λ f → is-decidable-Prop (∀' ℕ (λ n → is-true-Prop (f n)))) bool-WLPO : UU lzero bool-WLPO = type-Prop bool-prop-WLPO abstract WLPO-bool-WLPO : bool-WLPO → WLPO WLPO-bool-WLPO bool-wlpo P = rec-coproduct ( λ all-true-f → inl (λ n → is-in-decidable-subtype-is-true-map-bool P n (all-true-f n))) ( λ not-all-true-f → inr ( λ full-P → not-all-true-f ( λ n → is-true-map-bool-is-in-decidable-subtype P n (full-P n)))) ( bool-wlpo (map-equiv (map-bool-decidable-subtype-equiv ℕ) P)) bool-WLPO-level-WLPO : {l : Level} → level-WLPO l → bool-WLPO bool-WLPO-level-WLPO {l} wlpo f = rec-coproduct ( λ full-P → inl ( λ n → tr ( λ g → is-true (g n)) ( is-section-map-inv-equiv (map-bool-decidable-subtype-equiv ℕ) f) ( is-true-map-bool-is-in-decidable-subtype P n (full-P n)))) ( λ not-full-P → inr ( λ all-true-f → not-full-P ( λ n → is-in-decidable-subtype-is-true-map-bool ( P) ( n) ( inv-tr ( λ g → is-true (g n)) ( is-section-map-inv-equiv ( map-bool-decidable-subtype-equiv ℕ) ( f)) ( all-true-f n))))) ( wlpo P) where P : decidable-subtype l ℕ P = map-inv-equiv (map-bool-decidable-subtype-equiv ℕ) f level-WLPO-iff-bool-WLPO : (l : Level) → level-WLPO l ↔ bool-WLPO pr1 (level-WLPO-iff-bool-WLPO _) = bool-WLPO-level-WLPO pr2 (level-WLPO-iff-bool-WLPO _) bwlpo = WLPO-bool-WLPO bwlpo
The weak limited principle of omniscience at any level implies it at all levels
WLPO-level-WLPO : {l : Level} → level-WLPO l → WLPO WLPO-level-WLPO level-wlpo = WLPO-bool-WLPO (bool-WLPO-level-WLPO level-wlpo)
See also
- The principle of omniscience
- The limited principle of omniscience
- The lesser limited principle of omniscience
- Markov’s principle
External links
Taboos.WLPO
at TypeTopology- weak limited principle of omniscience at Lab
Recent changes
- 2025-04-25. Louis Wasserman. Reframe limited principle of omniscience and variants in terms of decidable subtypes (#1404).
- 2025-04-25. Fredrik Bakke. chore: Fix some links (#1411).
- 2025-01-07. Fredrik Bakke. Logic (#1226).
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).