The lesser limited principle of omniscience

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Maša Žaucer.

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

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

open import foundation.booleans
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.propositions
open import foundation-core.sets

Statement

The lesser limited principle of omniscience (LLPO) asserts that for any sequence of booleans f : ℕ → bool such that f n is true for at most one n, then either f n is false for all even n or f n is false for all odd n.

prop-LLPO : Prop lzero
prop-LLPO =
  ∀'
    ( ℕ → bool)
    ( λ f →
      function-Prop
        ( is-prop (Σ ℕ (λ n → is-true (f n))))
        ( disjunction-Prop
          ( ∀' ℕ (λ n → function-Prop (is-even-ℕ n) (is-false-Prop (f n))))
          ( ∀' ℕ (λ n → function-Prop (is-odd-ℕ n) (is-false-Prop (f n))))))

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

is-prop-LLPO : is-prop LLPO
is-prop-LLPO = is-prop-type-Prop prop-LLPO

See also

Recent changes