Foundation Primitive Recognition Calculus Omniscience Lpo Iff Wlpo And Markov

The exact location of LPO

In constructive mathematics, the Limited Principle of Omniscience (LPO) is a statement about infinite binary sequences: for any sequence of true and false values, either it is all false, or there is a place where it turns true. Classically this is a trivial tautology, but constructively it is a strong assumption, because it asserts that a search over infinitely many terms either finds a witness or is known to be empty. The framework's library, a machine-checked collection of formal theorems, proves that LPO is exactly the combination of two weaker principles.

The first weaker principle is the Weak Limited Principle of Omniscience (WLPO), which decides only whether the sequence is all false or not all false, without locating a witness. The second is Markov's Principle, which says that if a sequence is known not to be all false, then a search will eventually find a true term. Each of these is strictly weaker than LPO on its own. The theorem lpo_iff_wlpo_and_markov establishes the exact equivalence: LPO holds if and only if both WLPO and Markov's Principle hold. The proof is choice-free, meaning it does not rely on the axiom of choice.

The two directions are proved separately. From LPO, one gets WLPO by weakening the existential witness to a double negation, and one gets Markov's Principle by a direct implication. The reverse direction is the substantive one: given WLPO's global decision and Markov's guarantee that a known-to-succeed search terminates, one reconstructs the full existential witness of LPO. The theorem pins LPO exactly between the two weaker principles, showing that full omniscience is their conjunction and nothing more.

This result matters because it gives a precise decomposition of a common constructive assumption. A reader who wants to know how much omniscience a proof uses can now measure it in two independent coordinates: the global bit and the terminating search. The theorem does not claim that either WLPO or Markov's Principle is provable in pure constructive logic; both remain independent assumptions. It also does not claim that LPO is constructively valid, only that it is equivalent to the pair.

/-- **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⟩

/-- `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 ⇒ Markov`: full omniscience subsumes the known-to-halt search. Choice-free. -/
theorem lpo_imp_markov (h : LPO) : MarkovPrinciple := by
  intro α hne
  rcases h α with hall | hex
  · exact absurd hall hne
  · exact hex

/-- `WLPO ∧ Markov ⇒ LPO`: deciding the Π⁰₁ statement, plus the known-to-halt search,
recovers full omniscience. Choice-free. This pins `LPO` exactly between the two
weaker principles. -/
theorem wlpo_and_markov_imp_lpo (hw : WLPO) (hm : MarkovPrinciple) : LPO := by
  intro α
  rcases hw α with hall | hne
  · exact Or.inl hall
  · exact Or.inr (hm α hne)

What this page does not claim

The theorem does not claim that WLPO or Markov's Principle is provable in pure constructive logic. The theorem does not claim that LPO is constructively valid, only that it is equivalent to the conjunction of the two weaker principles.

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: