The 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.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.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.negation
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets

open import univalent-combinatorics.standard-finite-types

Statement

The limited principle of omniscience (LPO) asserts that for every sequence f : ℕ → bool there either exists an n such that f n is true, or f n is false for all n.

LPO : UU lzero
LPO =
  (f : ℕ → bool) →
  ( exists ℕ (λ n → is-true-Prop (f n))) +
  ( for-all ℕ (λ n → is-false-Prop (f n)))

Properties

The limited principle of omniscience is a proposition

is-prop-LPO : is-prop LPO
is-prop-LPO =
  is-prop-Π
    ( λ f →
      is-prop-coproduct
        ( elim-exists
          ( ¬' ∀' ℕ (λ n → is-false-Prop (f n)))
          ( λ n t h → not-is-false-is-true (f n) t (h n)))
        ( is-prop-exists ℕ (λ n → is-true-Prop (f n)))
        ( is-prop-for-all-Prop ℕ (λ n → is-false-Prop (f n))))

prop-LPO : Prop lzero
prop-LPO = LPO , is-prop-LPO

See also

Recent changes