The limited principle of omniscience

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

Created on 2022-08-08.
Last modified on 2024-04-11.

module where
open import elementary-number-theory.natural-numbers

open import foundation.disjunction
open import foundation.existential-quantification
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


The limited principle of omniscience (LPO) asserts that for every sequence f : ℕ → Fin 2 there either exists an n such that f n = 1 or for all n we have f n = 0.

LPO : UU lzero
  (f :   Fin 2) 
    (    n  Id-Prop (Fin-Set 2) (f n) (one-Fin 1)))
    ( ∀'   n  Id-Prop (Fin-Set 2) (f n) (zero-Fin 1)))

See also

Recent changes