Foundation Primitive Recognition Calculus Omniscience

Omniscience and its limits

Omniscience, in the mathematical sense studied here, is the ability to answer a question about an infinite list of yes-or-no entries. The classical idea is simple: for any infinite binary sequence, either every entry is false, or at least one entry is true. This statement, called the Limited Principle of Omniscience (LPO), is trivially true in classical mathematics, where every proposition is either true or false. But in constructive mathematics, where proofs must exhibit the objects they discuss, LPO is not provable. It asserts that one can decide, for any sequence, whether a true entry exists somewhere, without ever seeing the whole sequence.

The subject here formalizes this principle and its close relatives in a machine-checked library of formal theorems. It defines four principles. LPO says every binary sequence is either all false or has a true entry. The Weak Limited Principle of Omniscience (WLPO) says every binary sequence is either all false or not all false, a weaker claim that only decides the negation. Markov's Principle says that if a sequence is not all false, then it has a true entry, capturing the idea of a search that is known to succeed. The Lesser Limited Principle of Omniscience (LLPO) says that for a sequence with at most one true entry, either all even-indexed entries are false or all odd-indexed entries are false.

The library proves the relationships among these principles. LPO implies each of the other three. More precisely, it proves that LPO is exactly equivalent to the conjunction of WLPO and Markov's Principle. This is a precise decomposition: full omniscience is the combination of deciding the global question (WLPO) and having a terminating search that finds the witness (Markov). The proofs are choice-free, meaning they do not rely on the axiom of choice, and they are fully checked by the machine.

In Recognition Science, this subject establishes the precise logical content of what it means for a recognition process, a discrete record of events, to have complete knowledge. The framework models recognition as a cost-forced process, and this subject pins down the exact logical power needed to decide questions about infinite sequences. It shows that full omniscience is not a single indivisible assumption but a conjunction of two distinct capabilities: knowing whether a property holds globally, and being able to find a witness when it does. This decomposition is a theorem, not a definitional choice.

The practical consequence is that the framework can state precisely which logical assumptions its derivations require. When a proof in the framework needs to decide a question about an infinite sequence, the subject identifies exactly which of the two capabilities is being used. This makes the framework's logical footprint explicit and auditable, rather than relying on an implicit and possibly stronger assumption of omniscience.

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

/-- `LPO ⇒ LLPO`. Given the witness located by `LPO` and the at-most-one-true
hypothesis, every index of the other parity must be `false`. The parity split is the
omega-produced disjunction `n % 2 = 0 ∨ n % 2 = 1`, so the proof avoids the classical
`Nat.even_or_odd` and stays choice-free. -/
theorem lpo_imp_llpo (h : LPO) : LLPO := by
  intro α hone
  rcases h α with hall | ⟨n, hn⟩
  · exact Or.inl (fun k => hall (2 * k))
  · have hmod : n % 2 = 0 ∨ n % 2 = 1 := by omega
    rcases hmod with hpar | hpar
    · refine Or.inr (fun k => ?_)
      cases hb : α (2 * k + 1) with
      | false => rfl
      | true => exfalso; have := hone n (2 * k + 1) hn hb; omega
    · refine Or.inl (fun k => ?_)
      cases hb : α (2 * k) with
      | false => rfl
      | true => exfalso; have := hone n (2 * k) hn hb; omega

What this page does not claim

The subject does not prove that omniscience exists in any physical sense. The subject does not show that any recognition process actually achieves omniscience.

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: