Encyclopedia Delta Delta Kernel Sound Meta Lpo

ARTICLE 3 claims 2 theorems 1 model

Delta Kernel Sound Meta Lpo

A precise logical principle that says a search over natural numbers either finds an answer or proves none exists, and what it means for a proof checker to record its use.

Verify this page

The limited principle of omniscience

The limited principle of omniscience, or LPO, is a classical logical principle studied in constructive mathematics. It states that for any property P of natural numbers that is decidable, meaning each number either has P or does not, either there exists a number with P, or all numbers fail P. In plain terms: if you can test every number one by one, then either your search eventually succeeds or it is guaranteed to fail forever. The principle is called limited because it applies only to searches over natural numbers, not to arbitrary sets, and omniscient because it asserts a definite answer to a question no finite procedure could always settle.

The Recognition Science framework's machine-checked library of formal theorems defines this principle as the declaration MetaLPO. The declaration states that for any decidable predicate P on natural numbers, either there is an n with P n, or for all n, not P n. This is not a new axiom. It is a formal definition of a known principle, and its role is to be recorded when a proof uses it. The framework's kernel, the part that checks proofs, keeps a ledger of which logical principles each derivation actually requires. When a proof uses LPO, the ledger records that fact, and the kernel's soundness theorem supplies the principle only when the ledger says it was used.

This matters because the framework distinguishes between proofs that use classical omniscience principles and proofs that do not. A derivation with an empty ledger, meaning it used none of these principles, is certified as true without excluded middle, without LPO, and without Markov's principle. The declaration MetaLPO is what the ledger refers to when it reports that a proof did use the limited principle of omniscience. The kernel's own soundness proof is conditional: it grants LPO to a derivation only if the ledger posted the LPO flag, so the record of what a proof needs is honest and complete.

MetaLPO does not claim that LPO is true in the framework's canonical model, nor that it is false. It does not prove that any particular search succeeds or fails. It does not assert that the framework itself relies on LPO. The declaration only names the principle so the kernel can track its use. The framework's forced fragment, which uses no such principles, is certified without any omniscience at all, and MetaLPO is the marker that keeps that claim precise.

MODEL MetaLPO · IndisputableMonolith/DeltaKernel/Sound.lean
MetaLPO · IndisputableMonolith/DeltaKernel/Sound.lean:54 
/-- Metatheoretic limited principle of omniscience (arithmetical form). Content
of the LPO posit. -/
def MetaLPO : Prop :=
  ∀ (P : Nat → Prop), (∀ n, P n ∨ ¬ P n) → (∃ n, P n) ∨ (∀ n, ¬ P n)
THEOREM sound_cond · IndisputableMonolith/DeltaKernel/Sound.lean
sound_cond · IndisputableMonolith/DeltaKernel/Sound.lean:199 · truncated 
theorem sound_cond : ∀ (d : Deriv) (Γ : Ctx) (φ : DFormula) (O : Ledger),
    check Γ d = some (φ, O) → Gated O → ∀ ρ : Env, CtxSat ρ Γ → DFormula.sat ρ φ := by
  intro d
  induction d with
  | hyp i =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hg : Γ[i]? with
      | none => simp [hg] at hchk
      | some ψ =>
          simp only [hg, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hφ, _⟩ := hchk
          subst hφ
          exact hΓ ψ (mem_of_getElem? hg)
  | eqRefl t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      rfl
  | eqSubst hole t s dEq dT ihEq ihT =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hdE : check Γ dEq with
      | none => simp [hdE] at hchk
      | some cpE =>
          obtain ⟨cEq, o₁⟩ := cpE
          cases hdT : check Γ dT with
          | none => simp [hdE, hdT] at hchk
          | some cpT =>
              obtain ⟨cT, o₂⟩ := cpT
              simp only [hdE, hdT] at hchk
              split at hchk
              · rename_i h1
                split at hchk
                · rename_i h2
                  simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨hc, hO⟩ := hchk
                  subst hc; subst hO
                  have HE := ihEq Γ cEq o₁ hdE (Gated.union_left hG) ρ hΓ
                  have HT := ihT Γ cT o₂ hdT (Gated.union_right hG) ρ hΓ
                  rw [h1] at HE
                  rw [h2] at HT
                  have hts : t.eval ρ = s.eval ρ := HE
                  rw [DFormula.sat_subst0] at HT
                  rw [DFormula.sat_subst0]
                  rw [← hts]
                  exact HT
                · nomatch hchk
              · nomatch hchk
  | succNeZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DFormula.neg, DTerm.eval]
      omega
  | succInj d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | eq a b =>
              cases a with
              | succ ta =>
                  cases b with
                  | succ tb =>
                      simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
                      obtain ⟨hc, hO⟩ := hchk
                      subst hc; subst hO
                      have H := ih Γ (DFormula.eq (DTerm.succ ta) (DTerm.succ tb)) o hd hG ρ hΓ
                      simp only [DFormula.sat, DTerm.eval] at H ⊢
                      omega
                  | var _ => simp [hd] at hchk
                  | zero => simp [hd] at hchk
                  | add _ _ => simp [hd] at hchk
                  | mul _ _ => simp [hd] at hchk
              | var _ => simp [hd] at hchk
              | zero => simp [hd] at hchk
              | add _ _ => simp [hd] at hchk
              | mul _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _ _ => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | addZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      omega
  | addSucc t s =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      omega
  | mulZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp [DFormula.sat, DTerm.eval]
  | mulSucc t s =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      exact Nat.mul_succ (t.eval ρ) (s.eval ρ)
  | ind hole d0 dS ih0 ihS =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd0 : check Γ d0 with
      | none => simp [hd0] at hchk
      | some cp0 =>
          obtain ⟨c0, o₁⟩ := cp0
          cases hdS : check Γ dS with
          | none => simp [hd0, hdS] at hchk
          | some cpS =>
              obtain ⟨cS, o₂⟩ := cpS
              simp only [hd0, hdS] at hchk
              split at hchk
              · rename_i hc0
                split at hchk
                · rename_i hcS
                  simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨hc, hO⟩ := hchk
                  subst hc
                  have hbase : Gated (o₁.union o₂) := by
                    split at hO
                    · subst hO; exact hG
                    · subst hO; exact Gated.union_left hG
                  have H0 := ih0 Γ c0 o₁ hd0 (Gated.union_left hbase) ρ hΓ
                  have HS := ihS Γ cS o₂ hdS (Gated.union_right hbase) ρ hΓ
                  rw [hc0] at H0
                  rw [hcS] at HS
                  have H0' := (DFormula.sat_subst0 hole DTerm.zero ρ).mp H0
                  simp only [DFormula.sat] at HS
                  simp only [DFormula.sat]
                  intro n
                  induction n with
                  | zero => exact H0'
                  | succ k ihk => exact (DFormula.sat_stepSucc hole k ρ).mp (HS k ihk)
                · nomatch hchk
              · nomatch hchk
  | implIntro hole d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check (hole :: Γ) d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          simp only [DFormula.sat]
          intro hhole
          exact ih (hole :: Γ) c o hd hG ρ (CtxSat.cons hhole hΓ)
  | implElim d1 d2 ih1 ih2 =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd1 : check Γ d1 with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c1, o₁⟩ := cp1
          cases hd2 : check Γ d2 with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c2, o₂⟩ := cp2
              cases c1 with
              | impl a b =>
                  simp only [hd1, hd2] at hchk
                  split at hchk
                  · rename_i hcond
                    simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                    obtain ⟨hb, hO⟩ := hchk
                    subst hb; subst hO
                    have H1 := ih1 Γ (DFormula.impl a b) o₁ hd1 (Gated.union_left hG) ρ hΓ
                    have H2 := ih2 Γ c2 o₂ hd2 (Gated.union_right hG) ρ hΓ
                    rw [hcond] at H2
                    exact H1 H2
                  · nomatch hchk
              | eq _ _ => simp [hd1, hd2] at hchk
              | fls => simp [hd1, hd2] at hchk
              | conj _ _ => simp [hd1, hd2] at hchk
              | disj _ _ => simp [hd1, hd2] at hchk
              | all _ => simp [hd1, hd2] at hchk
              | ex _ => simp [hd1, hd2] at hchk
  | conjIntro d1 d2 ih1 ih2 =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd1 : check Γ d1 with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c1, o₁⟩ := cp1
          cases hd2 : check Γ d2 with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c2, o₂⟩ := cp2
              simp only [hd1, hd2, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H1 := ih1 Γ c1 o₁ hd1 (Gated.union_left hG) ρ hΓ
              have H2 := ih2 Γ c2 o₂ hd2 (Gated.union_right hG) ρ hΓ
              exact ⟨H1, H2⟩
  | conjElim1 d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | conj a b =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H := ih Γ (DFormula.conj a b) o hd hG ρ hΓ
              exact H.1
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | conjElim2 d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | conj a b =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H := ih Γ (DFormula.conj a b) o hd hG ρ hΓ
              exact H.2
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | disjIntro1 ψf d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          have H := ih Γ c o hd hG ρ hΓ
          exact Or.inl H
  | disjIntro2 φf d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          have H := ih Γ c o hd hG ρ hΓ
          exact Or.inr H
  | disjElim d dL dR ih ihL ihR =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | disj a b =>
              simp only [hd] at hchk
              cases hdL : check (a :: Γ) dL with
              | none => simp [hdL] at hchk
              | some cpL =>
                  obtain ⟨χ1, o₁⟩ := cpL
                  cases hdR : check (b :: Γ) dR with
                  | none => simp [hdL, hdR] at hchk
                  | some cpR =>
                      obtain ⟨χ2, o₂⟩ := cpR
                      simp only [hdL, hdR] at hchk
                      split at hchk
                      · rename_i hchi
                        simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                        obtain ⟨hc, hO⟩ := hchk
                        subst hc; subst hO
                        have Hd := ih Γ (DFormula.disj a b) o hd
                          (Gated.union_left (Gated.union_left hG)) ρ hΓ
                        simp only [DFormula.sat] at Hd
                        rcases Hd with ha | hb
                        · exact ihL (a :: Γ) χ1 o₁ hdL
                            (Gated.union_right (Gated.union_left hG)) ρ (CtxSat.cons ha hΓ)
                        · have HR := ihR (b :: Γ) χ2 o₂ hdR
                            (Gated.union_right hG) ρ (CtxSat.cons hb hΓ)
                          rw [hchi]
                          exact HR
                      · nomatch hchk
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _

-- … truncated for the page; open the module for the rest.
THEOREM sound_forced · IndisputableMonolith/DeltaKernel/Sound.lean
sound_forced · IndisputableMonolith/DeltaKernel/Sound.lean:663 
/-- FORCED soundness: a derivation the kernel accepts with the EMPTY ledger is
true in the canonical model, with NONE of the three metatheoretic principles.
The gates are discharged vacuously (`Gated.empty`), so the proof term never
touches EM/LPO/MP or `Classical.choice`. `#print axioms sound_forced` is the
kernel's own σ0 / DELTA_FORCED self-audit. -/
theorem sound_forced {d : Deriv} {φ : DFormula} (h : Forced [] d φ) :
    ∀ ρ : Env, DFormula.sat ρ φ := by
  intro ρ
  refine sound_cond d [] φ Ledger.empty h Gated.empty ρ ?_
  intro ψ hψ
  cases hψ

What this page does not claim

MetaLPO does not assert that the limited principle of omniscience is true or false in the framework's canonical model. MetaLPO does not prove that any particular search over natural numbers succeeds or fails. The framework's own forced fragment does not rely on LPO, and MetaLPO is not an axiom the framework assumes.

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/DeltaKernel/Sound.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND