LPO
plain-language theorem explainer
Limited Principle of Omniscience: every binary sequence is either identically false or true at some index. Equivalent to decidability of every Σ⁰₁ predicate on ℕ; constructively unprovable, classically trivial. Encodes the omniscience behind real-number trichotomy. Cited by the Omniscience hierarchy (WLPO, Markov, LLPO) and related forced-order work. Introduced as a bare Prop definition.
Claim. The Limited Principle of Omniscience asserts that for every sequence $\alpha:\mathbb{N}\to\{\mathrm{true},\mathrm{false}\}$, either $\alpha(n)=\mathrm{false}$ for all $n$, or there exists $n$ with $\alpha(n)=\mathrm{true}$. Equivalently, every $\Sigma^0_1$ predicate over the naturals is decidable.
background
This declaration sits in the Primitive Recognition Calculus Omniscience module, which packages the classical omniscience principles that appear when constructive foundations meet real-number and order facts.
LPO is the strongest of the limited omniscience principles on binary sequences $\alpha:\mathbb{N}\to\mathrm{Bool}$: either the sequence is identically false, or it hits true somewhere. The weaker sibling WLPO only decides the $\Pi^0_1$ statement (identically false or not), replacing the existential witness by a double negation. Markov's principle is the converse direction: non-identity-to-false yields a witness. LLPO is the parity-restricted form tied to the order dichotomy $0\le x\lor x\le 0$ and to exact intermediate-value facts.
Constructively these principles are independent of intuitionistic logic; classically they are theorems. The module records them as Props so downstream Recognition results can name exactly which omniscience is consumed rather than smuggling classical case splits.
proof idea
Pure definition: LPO is the Prop equal to
$\forall\alpha:\mathbb{N}\to\mathrm{Bool},\ (\forall n,\ \alpha n=\mathrm{false})\lor(\exists n,\ \alpha n=\mathrm{true})$.
There is no proof obligation beyond the defining equation. Downstream implication theorems unpack the disjunction by cases on that dichotomy (for example lpo_imp_wlpo, lpo_imp_markov, lpo_imp_llpo).
why it matters
LPO is the top of the omniscience ladder in this module. It implies WLPO, Markov's principle, and LLPO via the choice-free theorems lpo_imp_wlpo, lpo_imp_markov, and lpo_imp_llpo. With the converse wlpo_and_markov_imp_lpo it sits in a tight relationship with WLPO combined with Markov. The doc-comment identifies it as the omniscience content of real-number trichotomy.
Downstream, ForcedTrichotomy.leq_total_bool establishes totality of the forced structural order on DistinctionNat by induction with an empty axiom print, so the constructive order path does not silently assume LPO. In Recognition Science the value is bookkeeping: trichotomy-style and intermediate-value-style facts carry named omniscience that must be tracked when the foundation stays choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.