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 2026-05-05.

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.dependent-products-propositions
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.types-with-decidable-dependent-product-types
open import foundation.types-with-decidable-universal-quantifications
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 = has-decidable-∀-prop-Level l ℕ

level-WLPO : (l : Level) → UU (lsuc l)
level-WLPO l = has-decidable-∀-Level l ℕ

WLPO : UUω
WLPO = {l : Level} → level-WLPO l

Properties

WLPO is logically equivalent to decidable Π-types of ℕ

has-decidable-Π-level-ℕ-level-WLPO :
  {l : Level} → level-WLPO l → has-decidable-Π-Level l ℕ
has-decidable-Π-level-ℕ-level-WLPO =
  has-decidable-Π-Level-has-decidable-∀-Level

level-WLPO-has-decidable-Π-level-ℕ :
  {l : Level} → has-decidable-Π-Level l ℕ → level-WLPO l
level-WLPO-has-decidable-Π-level-ℕ =
  has-decidable-∀-Level-has-decidable-Π-Level

has-decidable-Π-ℕ-WLPO : WLPO → has-decidable-Π ℕ
has-decidable-Π-ℕ-WLPO = has-decidable-Π-has-decidable-∀

WLPO-has-decidable-Π-ℕ : has-decidable-Π ℕ → WLPO
WLPO-has-decidable-Π-ℕ = has-decidable-∀-has-decidable-Π

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

Recent changes