Foundation Primitive Recognition Calculus Omniscience Lpo Imp Wlpo

The implication

The Limited Principle of Omniscience (LPO) and the Weak Limited Principle of Omniscience (WLPO) are statements about binary sequences, infinite lists where each entry is either true or false. LPO asserts that for every such sequence, either all entries are false, or at least one entry is true. WLPO makes a weaker assertion: for every binary sequence, either all entries are false, or it is not the case that all entries are false. The difference is subtle but important in constructive mathematics, where the law of excluded middle is not assumed.

The theorem lpo_imp_wlpo establishes that LPO implies WLPO. If you can decide whether a sequence has a true entry, then you can certainly decide whether it is not the case that all entries are false. The proof is direct: if LPO gives you a witness, a specific position where the sequence is true, then you know the sequence is not all false. If LPO tells you the sequence is all false, then you have the first option of WLPO directly. The proof is choice-free, meaning it does not rely on the axiom of choice.

This implication is one step in a precise map of constructive principles. The framework's library, a machine-checked collection of formal theorems, also proves the converse direction in combination with Markov's Principle, which states that if a binary sequence is not all false, then it has a true entry. Together, these results show that LPO is exactly equivalent to the conjunction of WLPO and Markov's Principle. This pins down the precise logical content of full omniscience: it is the combination of a global bit of information and a terminating search.

The theorem does not claim that LPO or WLPO are true. They are principles that are constructively unprovable but classically trivial. The proof only establishes a relation between them, not their validity. It also does not claim that WLPO implies LPO, which is false without additional assumptions. The implication is one-way, and the framework is careful to state the direction explicitly.

/-- `LPO ⇒ WLPO`: deciding the Σ⁰₁ witness in particular decides its Π⁰₁ negation.
Choice-free. -/
theorem lpo_imp_wlpo (h : LPO) : WLPO := by
  intro α
  rcases h α with hall | ⟨n, hn⟩
  · exact Or.inl hall
  · exact Or.inr (fun hall => Bool.noConfusion ((hall n).symm.trans hn))

/-- `LPO ⇒ WLPO`: deciding the Σ⁰₁ witness in particular decides its Π⁰₁ negation.
Choice-free. -/
theorem lpo_imp_wlpo (h : LPO) : WLPO := by
  intro α
  rcases h α with hall | ⟨n, hn⟩
  · exact Or.inl hall
  · exact Or.inr (fun hall => Bool.noConfusion ((hall n).symm.trans hn))

/-- **The exact location of LPO**: `LPO ⇔ WLPO ∧ Markov`. The two coordinates
are the global bit (WLPO) and the terminating search (Markov); full omniscience
is exactly their conjunction. Choice-free. -/
theorem lpo_iff_wlpo_and_markov : LPO ↔ (WLPO ∧ MarkovPrinciple) :=
  ⟨fun h => ⟨lpo_imp_wlpo h, lpo_imp_markov h⟩,
   fun ⟨hw, hm⟩ => wlpo_and_markov_imp_lpo hw hm⟩

What this page does not claim

The theorem does not assert that LPO or WLPO are true principles. The theorem does not claim that WLPO implies LPO. The theorem does not rely on the law of excluded middle or the axiom of choice.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Omniscience.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: