lpo_imp_wlpo
plain-language theorem explainer
The limited principle of omniscience implies its weak form: if every binary sequence is either identically false or true somewhere, then every binary sequence is either identically false or not. Constructive reverse mathematicians, and anyone tracking which omniscience axioms Recognition Science assumes, would cite this. The proof is a short case split that turns an existential witness into a contradiction against the universal claim. Choice-free.
Claim. If the limited principle of omniscience holds—for every binary sequence $\alpha:\mathbb{N}\to\{0,1\}$, either $\forall n,\,\alpha(n)=0$ or $\exists n,\,\alpha(n)=1$—then the weak limited principle of omniscience holds: for every such $\alpha$, either $\forall n,\,\alpha(n)=0$ or $\neg(\forall n,\,\alpha(n)=0)$.
background
This module sits in the Primitive Recognition Calculus foundation layer and records the classical omniscience hierarchy used when Recognition Science talks about decidability of predicates on natural numbers (and, by extension, about real-number trichotomy).
The limited principle of omniscience asserts that every binary sequence is either identically false or hits true at some index. Equivalently, every $\Sigma^0_1$ predicate on $\mathbb{N}$ is decidable. It is constructively unprovable and classically trivial; the module notes it is the omniscience content of real-number trichotomy.
The weak limited principle of omniscience weakens the positive existential to a double negation: it decides the $\Pi^0_1$ statement "identically false" versus its negation, without producing a witness. Markov's principle and LLPO sit nearby in the same hierarchy.
proof idea
Fix an arbitrary binary sequence $\alpha$ and apply the limited principle of omniscience to it. The left disjunct ($\alpha$ is identically false) is already the left disjunct of the weak form. On the right disjunct one obtains a concrete index $n$ with $\alpha(n)=\mathsf{true}$. That witness immediately refutes the claim that $\alpha$ is identically false: assuming $\forall k,,\alpha(k)=\mathsf{false}$ yields $\alpha(n)=\mathsf{false}$, which contradicts $\alpha(n)=\mathsf{true}$ by Boolean discrimination. Hence $\neg(\forall n,,\alpha(n)=\mathsf{false})$, the right disjunct of the weak principle. No choice axiom is used.
why it matters
This is a standard, choice-free implication in the constructive omniscience hierarchy. Within the Recognition Science mirror it anchors the Primitive Recognition Calculus Omniscience module: full LPO is strictly stronger than WLPO, and the module also records the sibling implications LPO implies Markov, LPO implies LLPO, and the converse that WLPO together with Markov recovers LPO. No downstream theorems currently depend on this lemma (used-by is empty), so its role is local hierarchy bookkeeping: whenever a later argument assumes full omniscience, the weaker $\Pi^0_1$ decision principle is free. The result does not touch the forcing chain T0–T8, the J-cost, the eight-tick octave, or the phi-ladder; it is pure foundational hygiene for what "decidability of recognition predicates" may assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.