IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Omniscience

   1/-
   2  PrimitiveRecognitionCalculus/Omniscience.lean
   3
   4  The omniscience principles, as the UNITS in which the strength of a non-forced
   5  posit is measured.
   6
   7  Milan's companion paper (`Distinction, Initiality, and Recognition Quotients`)
   8  closes the CARDINALITY wall: a finite presentation generates a countable carrier,
   9  so the order-completion of ℚ (the continuum) is not finitely generated. That is a
  10  statement about SIZE. `PRCCompletenessIndependence` closes the MODEL-THEORETIC
  11  wall: order-completeness holds in ℝ and fails in a countable cost-closed field, so
  12  completeness is not ENTAILED by the cost/field axioms.
  13
  14  This module opens the third, sharper wall, which neither of those touches: the
  15  PROOF-THEORETIC strength of completeness. The question is not "is the completed
  16  object too big?" nor "is completeness independent?" but "exactly HOW MUCH logical
  17  omniscience does a completeness principle smuggle in?". The answer is read in the
  18  classical reverse-mathematics / constructive-reverse-mathematics currency: the
  19  Limited Principle of Omniscience and its relatives. Real-number trichotomy is
  20  analytic `LPO`; the order dichotomy `0 ≤ x ∨ x ≤ 0` is analytic `LLPO`; monotone
  21  convergence carries `LPO`. These principles are decisions about Σ⁰₁ data that
  22  distinction does not force (you cannot, from a finite certificate, decide whether a
  23  countable search halts), so a posit that entails one of them is exactly that much
  24  stronger than the δ base.
  25
  26  Here we fix the vocabulary and prove the part that is purely arithmetical and
  27  choice-free: the omniscience hierarchy itself (`LPO ⇒ WLPO`, `LPO ⇒ LLPO`,
  28  `LPO ⇒ Markov`, and `WLPO ∧ Markov ⇒ LPO`). The forward CALIBRATIONS that connect
  29  these to completeness (`trichotomy ⇒ LPO`, `dichotomy ⇒ LLPO`, `MCT ⇒ LPO`) live
  30  on a constructive real carrier and are grown as the next ladder rungs.
  31
  32  The principles are stated over `ℕ → Bool` (binary sequences = decidable Σ⁰₁
  33  predicates). As `Prop`s they are choice-free; the point is precisely that they are
  34  NOT provable from the δ base, while classically (with `Classical.em`) they are all
  35  true. We never invoke `Classical` here, so the hierarchy lemmas are constructively
  36  valid implications.
  37
  38  No project-local axioms. No sorry.
  39-/
  40
  41import Mathlib
  42
  43namespace IndisputableMonolith
  44namespace Foundation
  45namespace PrimitiveRecognitionCalculus
  46namespace Omniscience
  47
  48/-- **LPO**, the Limited Principle of Omniscience. For every binary sequence, either
  49it is identically `false`, or it is `true` somewhere. Equivalently: every Σ⁰₁
  50predicate over ℕ is decidable. Constructively unprovable; classically trivial. This
  51is the omniscience content of real-number trichotomy. -/
  52def LPO : Prop := ∀ α : ℕ → Bool, (∀ n, α n = false) ∨ (∃ n, α n = true)
  53
  54/-- **WLPO**, the Weak Limited Principle of Omniscience. For every binary sequence,
  55either it is identically `false`, or it is not. This is `LPO` with the positive
  56existential weakened to a double negation: it decides the Π⁰₁ statement, not its Σ⁰₁
  57witness. -/
  58def WLPO : Prop := ∀ α : ℕ → Bool, (∀ n, α n = false) ∨ ¬ (∀ n, α n = false)
  59
  60/-- **Markov's Principle**. If a binary sequence is not identically `false`, then it
  61is `true` somewhere. The constructive "unbounded search that is known to succeed does
  62succeed" principle. -/
  63def MarkovPrinciple : Prop := ∀ α : ℕ → Bool, ¬ (∀ n, α n = false) → ∃ n, α n = true
  64
  65/-- **LLPO**, the Lesser Limited Principle of Omniscience. For a binary sequence with
  66at most one `true` term, either all even-indexed terms are `false`, or all
  67odd-indexed terms are `false`. This is the omniscience content of the order dichotomy
  68`0 ≤ x ∨ x ≤ 0` and of the (exact) intermediate value theorem. Strictly weaker than
  69`LPO`. -/
  70def LLPO : Prop :=
  71  ∀ α : ℕ → Bool,
  72    (∀ m n, α m = true → α n = true → m = n) →
  73    ((∀ k, α (2 * k) = false) ∨ (∀ k, α (2 * k + 1) = false))
  74
  75/-- `LPO ⇒ WLPO`: deciding the Σ⁰₁ witness in particular decides its Π⁰₁ negation.
  76Choice-free. -/
  77theorem lpo_imp_wlpo (h : LPO) : WLPO := by
  78  intro α
  79  rcases h α with hall | ⟨n, hn⟩
  80  · exact Or.inl hall
  81  · exact Or.inr (fun hall => Bool.noConfusion ((hall n).symm.trans hn))
  82
  83/-- `LPO ⇒ Markov`: full omniscience subsumes the known-to-halt search. Choice-free. -/
  84theorem lpo_imp_markov (h : LPO) : MarkovPrinciple := by
  85  intro α hne
  86  rcases h α with hall | hex
  87  · exact absurd hall hne
  88  · exact hex
  89
  90/-- `LPO ⇒ LLPO`. Given the witness located by `LPO` and the at-most-one-true
  91hypothesis, every index of the other parity must be `false`. The parity split is the
  92omega-produced disjunction `n % 2 = 0 ∨ n % 2 = 1`, so the proof avoids the classical
  93`Nat.even_or_odd` and stays choice-free. -/
  94theorem lpo_imp_llpo (h : LPO) : LLPO := by
  95  intro α hone
  96  rcases h α with hall | ⟨n, hn⟩
  97  · exact Or.inl (fun k => hall (2 * k))
  98  · have hmod : n % 2 = 0 ∨ n % 2 = 1 := by omega
  99    rcases hmod with hpar | hpar
 100    · refine Or.inr (fun k => ?_)
 101      cases hb : α (2 * k + 1) with
 102      | false => rfl
 103      | true => exfalso; have := hone n (2 * k + 1) hn hb; omega
 104    · refine Or.inl (fun k => ?_)
 105      cases hb : α (2 * k) with
 106      | false => rfl
 107      | true => exfalso; have := hone n (2 * k) hn hb; omega
 108
 109/-- `WLPO ∧ Markov ⇒ LPO`: deciding the Π⁰₁ statement, plus the known-to-halt search,
 110recovers full omniscience. Choice-free. This pins `LPO` exactly between the two
 111weaker principles. -/
 112theorem wlpo_and_markov_imp_lpo (hw : WLPO) (hm : MarkovPrinciple) : LPO := by
 113  intro α
 114  rcases hw α with hall | hne
 115  · exact Or.inl hall
 116  · exact Or.inr (hm α hne)
 117
 118end Omniscience
 119end PrimitiveRecognitionCalculus
 120end Foundation
 121end IndisputableMonolith
 122