The limited principle of omniscience
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-08-08.
Last modified on 2023-06-08.
module foundation.limited-principle-of-omniscience where
Imports
open import elementary-number-theory.natural-numbers open import foundation.disjunction open import foundation.existential-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 : ℕ → Fin 2
there either exists an n
such that f n = 1
or for all n
we have f n = 0
.
LPO : UU lzero LPO = (f : ℕ → Fin 2) → type-disj-Prop ( ∃-Prop ℕ (λ n → f n = one-Fin 1)) ( Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1)))
See also
- The principle of omniscience
- The lesser limited principle of omniscience
- The weak limited principle of omniscience
Recent changes
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).