Theme/Logic.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Pigeonhole3import FrcCore.Shell4import FrcCore.Series56/-!7# FrcCore.Theme.Logic — the bounded language over a finite structure and its counting (the logic theme, task LM17)89An explicit language of `Δ₀` formulas with two evaluators, over `ℕ` and in a frame `W_N` where overflow makes an atom10false, and the bounded stability schema: every formula takes its standard value in every frame above its bound (5:B6).11The counting behind the paradoxes of infinity and finite Gödel: fewer than `s^(K+1)` records of length `≤ K` and no12mirror of a larger frame (5:C2; `no_mirror` is in the base's `Series.lean` since task LM23); an iteration on `n`13states repeats within `n` steps (5:C5, 5:E5); Cantor on the finite frame (5:D3); the least element (5:E1, 5:E2); on a14finite carrier an injective map is onto, a part with fewer states identifies two elements, `m + 1` sentences outnumber15`m` elements (25:C1, 25:C5, 25:D1); the count of a Boolean predicate; dense codings need `a^n ≤ m^k` (25:F4). Moved16from 5-reductio and 25-godel, whose modules keep every old name. No axioms.17-/1819namespace FRC.Logic2021/-! ### the maximum, from its definition -/2223/-- `mx a b`, the larger of two naturals, with its two bounds proved from the definition. -/24def mx (a b : Nat) : Nat := if a ≤ b then b else a2526theorem le_mx_left (a b : Nat) : a ≤ mx a b := by27  unfold mx28  match Nat.decLe a b with29  | isTrue h => rw [ite_eq_left h]; exact h30  | isFalse h => rw [ite_eq_right h]; exact Nat.le_refl a3132theorem le_mx_right (a b : Nat) : b ≤ mx a b := by33  unfold mx34  match Nat.decLe a b with35  | isTrue h => rw [ite_eq_left h]; exact Nat.le_refl b36  | isFalse h => rw [ite_eq_right h]; exact Nat.le_of_lt (Nat.lt_of_not_le h)3738theorem lt_of_mx_lt_left {a b N : Nat} (h : mx a b < N) : a < N := Nat.lt_of_le_of_lt (le_mx_left a b) h39theorem lt_of_mx_lt_right {a b N : Nat} (h : mx a b < N) : b < N := Nat.lt_of_le_of_lt (le_mx_right a b) h4041/-! ### 5:B6 — the bounded stability schema for an explicit `Δ₀` language -/4243/-- Terms: variables (de Bruijn indices), `0`, `1`, sum, product. -/44inductive Term where45  | var : Nat → Term46  | zero : Term47  | one : Term48  | add : Term → Term → Term49  | mul : Term → Term → Term5051/-- `Δ₀` formulas: atoms `s = t`, `s < t`, negation, conjunction, and the bounded quantifier `∀ x ≤ t, φ`52(`x` is variable `0` in `φ`, the other variables shift up; `t` is read in the outer environment). -/53inductive Form where54  | eq : Term → Term → Form55  | lt : Term → Term → Form56  | neg : Form → Form57  | conj : Form → Form → Form58  | ball : Term → Form → Form5960/-- The environment extended by a value for variable `0`. -/61def cons (x : Nat) (env : Nat → Nat) : Nat → Nat62  | 0 => x63  | i + 1 => env i6465/-- Terms over `ℕ`. -/66def evalT (env : Nat → Nat) : Term → Nat67  | .var i => env i68  | .zero => 069  | .one => 170  | .add s t => evalT env s + evalT env t71  | .mul s t => evalT env s * evalT env t7273/-- `f 0 && … && f (n − 1)`. -/74def allBelow (f : Nat → Bool) : Nat → Bool75  | 0 => true76  | n + 1 => f n && allBelow f n7778/-- Formulas over `ℕ` (the standard value). -/79def evalF (env : Nat → Nat) : Form → Bool80  | .eq s t => decide (evalT env s = evalT env t)81  | .lt s t => decide (evalT env s < evalT env t)82  | .neg φ => !(evalF env φ)83  | .conj φ ψ => evalF env φ && evalF env ψ84  | .ball t φ => allBelow (fun x => evalF (cons x env) φ) (evalT env t + 1)8586/-- Terms in the frame `W_N`: a value is defined only while every intermediate value stays below `N`87(overflow: `A(x, y, z)` fails for `x + y ≥ N`). -/88def evalT? (N : Nat) (env : Nat → Nat) : Term → Option Nat89  | .var i => if env i < N then some (env i) else none90  | .zero => if 0 < N then some 0 else none91  | .one => if 1 < N then some 1 else none92  | .add s t => match evalT? N env s, evalT? N env t with93      | some a, some b => if a + b < N then some (a + b) else none94      | some _, none => none95      | none, some _ => none96      | none, none => none97  | .mul s t => match evalT? N env s, evalT? N env t with98      | some a, some b => if a * b < N then some (a * b) else none99      | some _, none => none100      | none, some _ => none101      | none, none => none102103/-- Formulas in the frame `W_N`: an atom with an undefined term is false, a bounded quantifier is guarded by104the definedness of its bound (the transcription `φ*` of the paper). -/105def evalF? (N : Nat) (env : Nat → Nat) : Form → Bool106  | .eq s t => match evalT? N env s, evalT? N env t with107      | some a, some b => decide (a = b)108      | some _, none => false109      | none, some _ => false110      | none, none => false111  | .lt s t => match evalT? N env s, evalT? N env t with112      | some a, some b => decide (a < b)113      | some _, none => false114      | none, some _ => false115      | none, none => false116  | .neg φ => !(evalF? N env φ)117  | .conj φ ψ => evalF? N env φ && evalF? N env ψ118  | .ball t φ => match evalT? N env t with119      | some b => allBelow (fun x => evalF? N (cons x env) φ) (b + 1)120      | none => false121122/-- The largest value a term's evaluation touches. -/123def boundT (env : Nat → Nat) : Term → Nat124  | .var i => env i125  | .zero => 0126  | .one => 1127  | .add s t => mx (mx (boundT env s) (boundT env t)) (evalT env s + evalT env t)128  | .mul s t => mx (mx (boundT env s) (boundT env t)) (evalT env s * evalT env t)129130/-- `max (f 0, …, f (n − 1))`. -/131def maxBelow (f : Nat → Nat) : Nat → Nat132  | 0 => 0133  | n + 1 => mx (f n) (maxBelow f n)134135/-- `t(φ)`, the largest integer referenced in the evaluation of `φ` over `ℕ`. -/136def boundF (env : Nat → Nat) : Form → Nat137  | .eq s t => mx (boundT env s) (boundT env t)138  | .lt s t => mx (boundT env s) (boundT env t)139  | .neg φ => boundF env φ140  | .conj φ ψ => mx (boundF env φ) (boundF env ψ)141  | .ball t φ => mx (boundT env t) (maxBelow (fun x => boundF (cons x env) φ) (evalT env t + 1))142143theorem le_maxBelow (f : Nat → Nat) : ∀ {n x : Nat}, x < n → f x ≤ maxBelow f n144  | 0, x, hx => absurd hx (Nat.not_lt_zero x)145  | n + 1, x, hx =>146    match Nat.decEq x n with147    | isTrue e => by rw [e]; exact le_mx_left _ _148    | isFalse e =>149      have hlt : x < n := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hx) e150      Nat.le_trans (le_maxBelow f hlt) (le_mx_right _ _)151152theorem allBelow_congr {f g : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → f x = g x) → allBelow f n = allBelow g n153  | 0, _ => rfl154  | n + 1, h => by155    show (f n && allBelow f n) = (g n && allBelow g n)156    rw [h n (Nat.lt_succ_self n), allBelow_congr (fun x hx => h x (Nat.lt_succ_of_lt hx))]157158/-- 5:B6 (terms) — below its bound a term is defined in the frame, with its standard value. -/159theorem evalT_frame (N : Nat) (env : Nat → Nat) : ∀ (t : Term), boundT env t < N → evalT? N env t = some (evalT env t)160  | .var i, h => by161    have h' : env i < N := h162    show (if env i < N then some (env i) else none) = some (env i); rw [ite_eq_left h']163  | .zero, h => by164    have h' : 0 < N := h165    show (if 0 < N then some 0 else none) = some 0; rw [ite_eq_left h']166  | .one, h => by167    have h' : 1 < N := h168    show (if 1 < N then some 1 else none) = some 1; rw [ite_eq_left h']169  | .add s t, h => by170    have hs := evalT_frame N env s (lt_of_mx_lt_left (lt_of_mx_lt_left h))171    have ht := evalT_frame N env t (lt_of_mx_lt_right (lt_of_mx_lt_left h))172    show (match evalT? N env s, evalT? N env t with173      | some a, some b => if a + b < N then some (a + b) else none174      | some _, none => none175      | none, some _ => none176      | none, none => none) = some (evalT env s + evalT env t)177    rw [hs, ht]178    show (if evalT env s + evalT env t < N then some (evalT env s + evalT env t) else none) = some (evalT env s + evalT env t)179    rw [ite_eq_left (lt_of_mx_lt_right h)]180  | .mul s t, h => by181    have hs := evalT_frame N env s (lt_of_mx_lt_left (lt_of_mx_lt_left h))182    have ht := evalT_frame N env t (lt_of_mx_lt_right (lt_of_mx_lt_left h))183    show (match evalT? N env s, evalT? N env t with184      | some a, some b => if a * b < N then some (a * b) else none185      | some _, none => none186      | none, some _ => none187      | none, none => none) = some (evalT env s * evalT env t)188    rw [hs, ht]189    show (if evalT env s * evalT env t < N then some (evalT env s * evalT env t) else none) = some (evalT env s * evalT env t)190    rw [ite_eq_left (lt_of_mx_lt_right h)]191192/-- 5:B6, 29:E2, 29:X2 (Theorem stability, schema form) — every `Δ₀` formula takes its standard value in every frame `W_N`193with `N > t(φ)`: `W_N ⊨ φ* ⟺ ℕ ⊨ φ`, for every environment, by induction on the formula. -/194theorem stable (N : Nat) : ∀ (φ : Form) (env : Nat → Nat), boundF env φ < N → evalF? N env φ = evalF env φ195  | .eq s t, env, h => by196    show (match evalT? N env s, evalT? N env t with197      | some a, some b => decide (a = b)198      | some _, none => false199      | none, some _ => false200      | none, none => false) = decide (evalT env s = evalT env t)201    rw [evalT_frame N env s (lt_of_mx_lt_left h), evalT_frame N env t (lt_of_mx_lt_right h)]202  | .lt s t, env, h => by203    show (match evalT? N env s, evalT? N env t with204      | some a, some b => decide (a < b)205      | some _, none => false206      | none, some _ => false207      | none, none => false) = decide (evalT env s < evalT env t)208    rw [evalT_frame N env s (lt_of_mx_lt_left h), evalT_frame N env t (lt_of_mx_lt_right h)]209  | .neg φ, env, h => by210    show (!(evalF? N env φ)) = !(evalF env φ)211    rw [stable N φ env h]212  | .conj φ ψ, env, h => by213    show (evalF? N env φ && evalF? N env ψ) = (evalF env φ && evalF env ψ)214    rw [stable N φ env (lt_of_mx_lt_left h), stable N ψ env (lt_of_mx_lt_right h)]215  | .ball t φ, env, h => by216    show (match evalT? N env t with217      | some b => allBelow (fun x => evalF? N (cons x env) φ) (b + 1)218      | none => false) = allBelow (fun x => evalF (cons x env) φ) (evalT env t + 1)219    rw [evalT_frame N env t (lt_of_mx_lt_left h)]220    show allBelow (fun x => evalF? N (cons x env) φ) (evalT env t + 1) = allBelow (fun x => evalF (cons x env) φ) (evalT env t + 1)221    exact allBelow_congr (fun x hx =>222      stable N φ (cons x env) (Nat.lt_of_le_of_lt (le_maxBelow (fun x => boundF (cons x env) φ) hx) (lt_of_mx_lt_right h)))223224/-! ### 5:C2 — records and the mirror -/225226/-- The number of strings of length at most `K` over `s` letters, `Σ_{i ≤ K} s^i`. -/227def records (s : Nat) : Nat → Nat228  | 0 => 1229  | K + 1 => records s K + s ^ (K + 1)230231/-- 5:C2, 29:C10 (the count) — fewer than `s^(K+1)` records exist for an alphabet of `s ≥ 2` letters. -/232theorem records_lt (s : Nat) (hs : 2 ≤ s) : ∀ K, records s K < s ^ (K + 1)233  | 0 => by234    show 1 < s ^ 1235    rw [Nat.pow_succ, Nat.pow_zero, Nat.one_mul]236    exact Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) hs237  | K + 1 => by238    show records s K + s ^ (K + 1) < s ^ (K + 1 + 1)239    have h1 : records s K + s ^ (K + 1) < s ^ (K + 1) + s ^ (K + 1) := Nat.add_lt_add_right (records_lt s hs K) _240    have h2 : s ^ (K + 1) + s ^ (K + 1) ≤ s ^ (K + 1) * s := by241      rw [← Nat.mul_two]; exact Nat.mul_le_mul_left _ hs242    exact Nat.lt_of_lt_of_le h1 h2243244/-! ### 5:C5, 5:E5 — an iteration on finitely many states repeats: periodic König and bounded halting -/245246/-- `iter f x k = f^k x`. -/247def iter (f : Nat → Nat) (x : Nat) : Nat → Nat248  | 0 => x249  | k + 1 => f (iter f x k)250251theorem iter_lt (f : Nat → Nat) {n : Nat} (hf : ∀ y, y < n → f y < n) {x : Nat} (hx : x < n) :252    ∀ k, iter f x k < n253  | 0 => hx254  | k + 1 => hf _ (iter_lt f hf hx k)255256theorem iter_add (f : Nat → Nat) (x : Nat) (i : Nat) : ∀ k, iter f x (i + k) = iter f (iter f x i) k257  | 0 => rfl258  | k + 1 => by show f (iter f x (i + k)) = f (iter f (iter f x i) k); rw [iter_add f x i k]259260/-- 5:E5, 5:C5 (Lemma periodic König, the pigeonhole) — on `n` states the iteration from `x` revisits a state within261`n` steps: some `i < j ≤ n` have `f^i x = f^j x`. -/262theorem repeat_below (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (x : Nat) (hx : x < n) :263    ∃ i j, i < j ∧ j ≤ n ∧ iter f x i = iter f x j :=264  have dec : Decidable (∃ j, j < n + 1 ∧ ∃ i, i < j ∧ iter f x i = iter f x j) :=265    @FRC.Shell.decExistsLT (fun j => ∃ i, i < j ∧ iter f x i = iter f x j)266      (fun j => FRC.Shell.decExistsLT (fun i => iter f x i = iter f x j) j) (n + 1)267  match dec with268  | isTrue ⟨j, hj, i, hij, e⟩ => ⟨i, j, hij, Nat.le_of_lt_succ hj, e⟩269  | isFalse hno =>270    have hinj : ∀ i j, i < n + 1 → j < n + 1 → iter f x i = iter f x j → i = j := fun i j hi hj e =>271      match Nat.lt_or_ge i j with272      | Or.inl hlt => absurd ⟨j, hj, i, hlt, e⟩ hno273      | Or.inr hge => match Nat.lt_or_ge j i with274        | Or.inl hlt => absurd ⟨i, hi, j, hlt, e.symm⟩ hno275        | Or.inr hge' => Nat.le_antisymm hge' hge276    have hnd := FRC.Shell.imageList_nodup hinj (Nat.le_refl (n + 1))277    have hb : ∀ e, Pigeonhole.mem e (FRC.Shell.imageList (iter f x) (n + 1)) → e < n := fun _ he =>278      match FRC.Shell.mem_imageList he with279      | ⟨k, _, ek⟩ => ek ▸ iter_lt f hf hx k280    have := Pigeonhole.length_le_of_nodup_lt n _ hnd hb281    by rw [FRC.Shell.imageList_length] at this; exact absurd this (Nat.not_succ_le_self n)282283theorem sub_pos {i j : Nat} (h : i < j) : 0 < j - i :=284  match Nat.decEq (j - i) 0 with285  | isTrue e =>286    have hj : j = i := by rw [← FRC.Nat.add_sub_of_le (Nat.le_of_lt h), e, Nat.add_zero]287    absurd (hj ▸ h) (Nat.lt_irrefl i)288  | isFalse e => Nat.pos_of_ne_zero e289290/-- 5:E5 — the walk is eventually periodic: from step `i` on, period `p = j − i` with `0 < p ≤ n`,291`f^(i+k+p) x = f^(i+k) x` for every `k`. -/292theorem eventually_periodic (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (x : Nat) (hx : x < n) :293    ∃ i p, 0 < p ∧ p ≤ n ∧ ∀ k, iter f x (i + k + p) = iter f x (i + k) :=294  match repeat_below f n hf x hx with295  | ⟨i, j, hij, hjn, e⟩ =>296    ⟨i, j - i, sub_pos hij, Nat.le_trans (Nat.sub_le j i) hjn, fun k => by297      rw [Nat.add_right_comm, FRC.Nat.add_sub_of_le (Nat.le_of_lt hij), iter_add f x j k, iter_add f x i k, e]⟩298299/-- 5:C5 (horizon separation) — a run on `n` states reaches a state `h` iff it reaches it within `n` steps: halting for bounded space is decided from above by `n` steps of simulation. -/300theorem halts_iff_halts_below (f : Nat → Nat) (n : Nat) (hf : ∀ y, y < n → f y < n) (h : Nat)301    (x : Nat) (hx : x < n) : (∃ k, iter f x k = h) ↔ ∃ k, k ≤ n ∧ iter f x k = h :=302  ⟨fun ⟨k, hk⟩ =>303    match repeat_below f n hf x hx with304    | ⟨i, j, hij, hjn, e⟩ =>305      match Nat.lt_or_ge k j with306      | Or.inl hkj => ⟨k, Nat.le_of_lt (Nat.lt_of_lt_of_le hkj hjn), hk⟩307      | Or.inr hjk =>308        -- the run is periodic from `i` with period `p = j − i`; reduce `k − i` modulo `p`309        have hp : 0 < j - i := sub_pos hij310        have per : ∀ q r, iter f x (i + (r + (j - i) * q)) = iter f x (i + r) := fun q r => by311          induction q with312          | zero => rw [Nat.mul_zero, Nat.add_zero]313          | succ q ih =>314            rw [Nat.mul_succ, ← Nat.add_assoc r ((j - i) * q) (j - i), Nat.add_comm (r + (j - i) * q) (j - i),315              ← Nat.add_assoc i (j - i) (r + (j - i) * q), FRC.Nat.add_sub_of_le (Nat.le_of_lt hij), iter_add f x j,316              ← e, ← iter_add f x i, ih]317        match FRC.Nat.mod_spec (j - i) hp (k - i) with318        | ⟨q, hq⟩ =>319          have hr : (k - i) % (j - i) < j - i := Nat.mod_lt _ hp320          have hk' : k = i + ((k - i) % (j - i) + (j - i) * q) := by321            rw [Nat.add_comm ((k - i) % (j - i)) _, ← hq, FRC.Nat.add_sub_of_le (Nat.le_trans (Nat.le_of_lt hij) hjk)]322          ⟨i + (k - i) % (j - i),323            Nat.le_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_left hr i)324              (by rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hij)]; exact hjn)),325            by rw [← per q, ← hk']; exact hk⟩,326   fun ⟨k, _, hk⟩ => ⟨k, hk⟩⟩327328/-! ### 5:D3 — Cantor's theorem on the finite frame -/329330/-- 5:D3 (Remark, the external diagonal) — Cantor's theorem holds in every finite frame: `n < 2^n`. -/331theorem cantor_finite (n : Nat) : n < 2 ^ n := Nat.lt_two_pow_self332333/-! ### 5:E1, 5:E2 — definable choice by the least element -/334335/-- The least `x < n` with `P x`, if any: the choice function `ch(A) = min A` of Definition global-choice. -/336def leastBelow (P : Nat → Bool) : Nat → Option Nat337  | 0 => none338  | n + 1 => match leastBelow P n with339    | some x => some x340    | none => if P n then some n else none341342/-- 5:E1, 29:B6 — a nonempty family has a choice: if some `x < n` has `P x`, `leastBelow P n` is defined. -/343theorem leastBelow_some (P : Nat → Bool) : ∀ (n x : Nat), x < n → P x = true → ∃ y, leastBelow P n = some y344  | 0, x, hx, _ => absurd hx (Nat.not_lt_zero x)345  | n + 1, x, hx, hP =>346    match hl : leastBelow P n with347    | some y => ⟨y, by348        show (match leastBelow P n with349          | some x => some x350          | none => if P n then some n else none) = some y351        rw [hl]⟩352    | none =>353      match Nat.decEq x n with354      | isTrue e => ⟨n, by355          show (match leastBelow P n with356            | some x => some x357            | none => if P n then some n else none) = some n358          rw [hl]359          show (if P n then some n else none) = some n360          have hPn : P n = true := e ▸ hP361          rw [hPn, ite_eq_left rfl]⟩362      | isFalse e =>363        absurd (leastBelow_some P n x (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hx) e) hP)364          (fun ⟨z, hz⟩ => nomatch (hl ▸ hz : (none : Option Nat) = some z))365366/-- 5:E1, 29:B6, 29:E2 (Proposition finite-choice) — the choice is a member, below the bound, and the least one. -/367theorem leastBelow_spec (P : Nat → Bool) : ∀ (n x : Nat), leastBelow P n = some x →368    x < n ∧ P x = true ∧ ∀ y, y < x → P y = false369  | 0, x, h => nomatch (h : (none : Option Nat) = some x)370  | n + 1, x, h => by371    have h' : (match leastBelow P n with372      | some x => some x373      | none => if P n then some n else none) = some x := h374    clear h375    revert h'376    match hl : leastBelow P n with377    | some y =>378      intro h'379      have e : y = x := Option.some.inj h'380      have := leastBelow_spec P n y hl381      exact ⟨Nat.lt_succ_of_lt (e ▸ this.1), e ▸ this.2.1, e ▸ this.2.2⟩382    | none =>383      intro h'384      have h'' : (if P n then some n else none) = some x := h'385      match hP : P n with386      | true =>387        rw [hP, ite_eq_left rfl] at h''388        have e : n = x := Option.some.inj h''389        refine ⟨Nat.lt_succ_of_le (Nat.le_of_eq e.symm), e ▸ hP, fun y hy => ?_⟩390        match hPy : P y with391        | false => rfl392        | true =>393          exact absurd (leastBelow_some P n y (e.symm ▸ hy) hPy)394            (fun ⟨z, hz⟩ => nomatch (hl ▸ hz : (none : Option Nat) = some z))395      | false =>396        rw [hP, ite_eq_right Bool.false_ne_true] at h''397        exact nomatch (h'' : (none : Option Nat) = some x)398399/-- 5:E2 (Lemma periodic choice) — the choice depends on the set alone: pointwise equal families choose alike,400so an equality-periodic family `A_{i+N} = A_i` has a choice function of the same period. -/401theorem leastBelow_congr {P Q : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → P x = Q x) → leastBelow P n = leastBelow Q n402  | 0, _ => rfl403  | n + 1, h => by404    show (match leastBelow P n with405      | some x => some x406      | none => if P n then some n else none) = (match leastBelow Q n with407      | some x => some x408      | none => if Q n then some n else none)409    rw [leastBelow_congr (fun x hx => h x (Nat.lt_succ_of_lt hx)), h n (Nat.lt_succ_self n)]410411/-! ### The counting core of 25-godel -/412413theorem or_intro_left {a b : Bool} (h : a = true) : (a || b) = true := by rw [h]; rfl414415theorem or_intro_right {a b : Bool} (h : b = true) : (a || b) = true := by rw [h]; cases a <;> rfl416417theorem and_true' (c : Bool) : (c && true) = c := by cases c <;> rfl418419theorem and_false' (c : Bool) : (c && false) = false := by cases c <;> rfl420421theorem and_self' (c : Bool) : (c && c) = c := by cases c <;> rfl422423theorem or_false' (c : Bool) : (c || false) = c := by cases c <;> rfl424425theorem and_assoc' (a b c : Bool) : ((a && b) && c) = (a && (b && c)) := by cases a <;> rfl426427/-- 25:C1, 29:B5 (Proposition noQ, the pigeonhole) — on `[0, n)` an injective map is onto: every `z < n` is a value. -/428theorem inj_onto (n : Nat) (S : Nat → Nat) (hS : ∀ x, x < n → S x < n)429    (hinj : ∀ x y, x < n → y < n → S x = S y → x = y) (z : Nat) (hz : z < n) : ∃ x, x < n ∧ S x = z :=430  have hnd := FRC.Shell.imageList_nodup hinj (Nat.le_refl n)431  have hlen := FRC.Shell.imageList_length S n432  have hb : ∀ e, Pigeonhole.mem e (FRC.Shell.imageList S n) → e < n := fun _ he =>433    match FRC.Shell.mem_imageList he with434    | ⟨j, hj, ej⟩ => ej ▸ hS j hj435  FRC.Shell.mem_imageList (Pigeonhole.mem_of_nodup_of_length_lt n _ hnd hb hlen z hz)436437/-- 25:C1, 29:B4, 29:B5 (Proposition noQ) — no successor of `Q` on a finite carrier: no map of `[0, n)` into itself is438injective and omits an element, so no finite structure is a model of `Q`. -/439theorem no_finite_successor (n : Nat) (S : Nat → Nat) (hS : ∀ x, x < n → S x < n)440    (hinj : ∀ x y, x < n → y < n → S x = S y → x = y) (z : Nat) (hz : z < n) : ¬ ∀ x, x < n → S x ≠ z :=441  fun hmiss => match inj_onto n S hS hinj z hz with442    | ⟨x, hx, e⟩ => hmiss x hx e443444/-- 25:D1 (Theorem part) — an agent with `R` storage states in a structure of `m > R` elements has no injective445encoding: every reading `ρ : [0, m) → [0, R)` identifies two elements. -/446theorem part_collides {m R : Nat} (hR : R < m) (ρ : Nat → Nat) (hρ : ∀ i, i < m → ρ i < R) :447    ¬ ∀ i j, i < m → j < m → ρ i = ρ j → i = j :=448  fun hinj => no_mirror hR ρ hρ hinj449450/-- 25:C5 (Remark Tarski scoped, the count) — `m + 1` sentences, indexed `0, …, m` (the row's sentences451`φ, ¬φ, …, ¬^m φ`), admit no injective numbering into a structure of `m` elements. -/452theorem sentences_outnumber (m : Nat) (g : Nat → Nat) (hg : ∀ i, i < m + 1 → g i < m) :453    ¬ ∀ i j, i < m + 1 → j < m + 1 → g i = g j → i = j :=454  part_collides (Nat.lt_succ_self m) g hg455456/-- The number of `i < n` with `f i = true`. -/457def count (f : Nat → Bool) : Nat → Nat458  | 0 => 0459  | n + 1 => count f n + cond (f n) 1 0460461theorem count_full {f : Nat → Bool} : ∀ {n : Nat}, (∀ i, i < n → f i = true) → count f n = n462  | 0, _ => rfl463  | n + 1, h => by464    show count f n + cond (f n) 1 0 = n + 1465    rw [h n (Nat.lt_succ_self n), count_full (fun i hi => h i (Nat.lt_succ_of_lt hi))]; rfl466467theorem cond_or_le (a b : Bool) : cond (a || b) 1 0 ≤ cond a 1 0 + cond b 1 0 := by468  cases a <;> cases b <;> decide469470theorem count_or_le (f g : Nat → Bool) : ∀ n, count (fun i => f i || g i) n ≤ count f n + count g n471  | 0 => Nat.le_refl 0472  | n + 1 => by473    show count (fun i => f i || g i) n + cond (f n || g n) 1 0 ≤ (count f n + cond (f n) 1 0) + (count g n + cond (g n) 1 0)474    rw [FRC.Nat.add_add_add_comm (count f n) (cond (f n) 1 0) (count g n) (cond (g n) 1 0)]475    exact Nat.add_le_add (count_or_le f g n) (cond_or_le (f n) (g n))476477theorem count_shift (f : Nat → Bool) : ∀ n, count (fun i => f (i + 1)) n ≤ count f (n + 1)478  | 0 => Nat.zero_le _479  | n + 1 => by480    show count (fun i => f (i + 1)) n + cond (f (n + 1)) 1 0 ≤ count f (n + 1) + cond (f (n + 1)) 1 0481    exact Nat.add_le_add_right (count_shift f n) _482483theorem count_false : ∀ n, count (fun _ => false) n = 0484  | 0 => rfl485  | n + 1 => by486    show count (fun _ => false) n + 0 = 0487    rw [count_false n]488489theorem count_single (j : Nat) : ∀ n, count (fun i => decide (j = i)) n ≤ 1 ∧ (n ≤ j → count (fun i => decide (j = i)) n = 0)490  | 0 => ⟨Nat.zero_le 1, fun _ => rfl⟩491  | n + 1 =>492    match Nat.decEq j n with493    | isTrue e => by494      have h0 : count (fun i => decide (j = i)) n = 0 := (count_single j n).2 (e ▸ Nat.le_refl j)495      refine ⟨?_, fun hle => absurd (e ▸ hle : n + 1 ≤ n) (Nat.not_succ_le_self n)⟩496      show count (fun i => decide (j = i)) n + cond (decide (j = n)) 1 0 ≤ 1497      rw [h0, decide_eq_true e]; exact Nat.le_refl 1498    | isFalse e => by499      refine ⟨?_, fun hle => ?_⟩500      · show count (fun i => decide (j = i)) n + cond (decide (j = n)) 1 0 ≤ 1501        rw [decide_eq_false e]; exact (count_single j n).1502      · show count (fun i => decide (j = i)) n + cond (decide (j = n)) 1 0 = 0503        rw [decide_eq_false e]; exact (count_single j n).2 (Nat.le_of_succ_le hle)504505theorem count_shift_by : ∀ (j : Nat) (f : Nat → Bool) (N : Nat), count (fun i => f (i + j)) N ≤ count f (N + j)506  | 0, _, _ => Nat.le_refl _507  | j + 1, f, N => Nat.le_trans (count_shift_by j (fun k => f (k + 1)) N) (count_shift f (N + j))508509/-- 25:F4 (Lemma density, the count) — an injective coding of the `a^n` strings of length `n` into `k`-tuples510over `m` elements needs `a^n ≤ m^k`. -/511theorem dense_coding {a n m k : Nat} (c : Nat → Nat) (hc : ∀ i, i < a ^ n → c i < m ^ k)512    (hinj : ∀ i j, i < a ^ n → j < a ^ n → c i = c j → i = j) : a ^ n ≤ m ^ k :=513  match Nat.lt_or_ge (m ^ k) (a ^ n) with514  | Or.inl h => absurd hinj (part_collides h c hc)515  | Or.inr h => h516517/-- A strict power step: `m < b` gives `m^(k+1) < b^(k+1)`. -/518theorem pow_lt_pow_base {m b : Nat} (h : m < b) : ∀ k : Nat, m ^ (k + 1) < b ^ (k + 1)519  | 0 => show m ^ 0 * m < b ^ 0 * b from Nat.mul_lt_mul_of_le_of_lt (Nat.le_refl 1) h (Nat.zero_lt_succ 0)520  | k + 1 => show m ^ (k + 1) * m < b ^ (k + 1) * b from Nat.mul_lt_mul_of_lt_of_lt (pow_lt_pow_base h k) h521522/-- 25:F4 (Lemma density, the digit form) — if `m` has at most `d` digits in base `a` (`m < a^d`), a coding of523the strings of length `n` by tuples of `k+1` coordinates with `a^n ≤ m^(k+1)` has `n < d·(k+1)`: a tuple carries524fewer letters than `d` times its coordinates. -/525theorem digit_bound {a n m k d : Nat} (ha : 0 < a) (hm : m < a ^ d) (h : a ^ n ≤ m ^ (k + 1)) :526    n < d * (k + 1) :=527  match Nat.lt_or_ge n (d * (k + 1)) with528  | Or.inl hlt => hlt529  | Or.inr hge =>530    have h1 : m ^ (k + 1) < (a ^ d) ^ (k + 1) := pow_lt_pow_base hm k531    have h2 : a ^ (d * (k + 1)) = (a ^ d) ^ (k + 1) := FRC.Nat.pow_mul a d (k + 1)532    have h3 : a ^ (d * (k + 1)) ≤ a ^ n := Nat.pow_le_pow_right ha hge533    absurd (Nat.lt_of_le_of_lt h (h2 ▸ h1)) (Nat.not_lt.mpr h3)534535/-- `f 0 || … || f (n − 1)`. -/536def anyBelow (f : Nat → Bool) : Nat → Bool537  | 0 => false538  | n + 1 => f n || anyBelow f n539540theorem anyBelow_congr {f g : Nat → Bool} : ∀ {n : Nat}, (∀ x, x < n → f x = g x) → anyBelow f n = anyBelow g n541  | 0, _ => rfl542  | n + 1, h => by543    show (f n || anyBelow f n) = (g n || anyBelow g n)544    rw [h n (Nat.lt_succ_self n), anyBelow_congr (fun x hx => h x (Nat.lt_succ_of_lt hx))]545546theorem anyBelow_false : ∀ n, anyBelow (fun _ => false) n = false547  | 0 => rfl548  | n + 1 => by549    show (false || anyBelow (fun _ => false) n) = false550    rw [anyBelow_false n]; rfl551552theorem allBelow_const (b : Bool) : ∀ n, 0 < n → allBelow (fun _ => b) n = b553  | 0, h => absurd h (Nat.lt_irrefl 0)554  | 1, _ => and_true' b555  | n + 2, _ => by556    show (b && allBelow (fun _ => b) (n + 1)) = b557    rw [allBelow_const b (n + 1) (Nat.succ_pos n)]; exact and_self' b558559theorem anyBelow_and_const (c : Bool) (F : Nat → Bool) (n : Nat) :560    anyBelow (fun x => c && F x) n = (c && anyBelow F n) := by561  cases c562  · exact anyBelow_false n563  · rfl564565theorem allBelow_and_const (c : Bool) (F : Nat → Bool) (n : Nat) (hn : 0 < n) :566    allBelow (fun y => c && F y) n = (c && allBelow F n) := by567  cases c568  · exact allBelow_const false n hn569  · rfl570571/-- Among the `x < n`, the clause `x = y` picks `y`: `∃ x < n, (c ∧ x = y ∧ F x)` is `c ∧ F y` for `y < n`. -/572theorem anyBelow_pick (c : Bool) (F : Nat → Bool) (y : Nat) :573    ∀ n, anyBelow (fun x => (c && decide (x = y)) && F x) n = (if y < n then c && F y else false)574  | 0 => rfl575  | n + 1 => by576    show (((c && decide (n = y)) && F n) || anyBelow (fun x => (c && decide (x = y)) && F x) n) = (if y < n + 1 then c && F y else false)577    rw [anyBelow_pick c F y n]578    exact match Nat.decEq n y with579    | isTrue e => by580      rw [decide_eq_true e, and_true' c, ite_eq_right (e ▸ Nat.lt_irrefl n : ¬ y < n), or_false', ite_eq_left (e ▸ Nat.lt_succ_self n : y < n + 1), e]581    | isFalse e => by582      rw [decide_eq_false e, and_false' c]583      show (if y < n then c && F y else false) = (if y < n + 1 then c && F y else false)584      exact match Nat.decLt y n with585      | isTrue hlt => by rw [ite_eq_left hlt, ite_eq_left (Nat.lt_succ_of_lt hlt)]586      | isFalse hge => by587        have hne : ¬ y < n + 1 := fun h => hge (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h) (fun e' => e e'.symm))588        rw [ite_eq_right hge, ite_eq_right hne]589590/-! ### 25:C2, 25:C3, 00:Z1 — the first-order theory of a finite structure: decidable, complete, consistent -/591592/-- A finite relational structure: the elements `0, …, m − 1` and decidable relations, `rel r xs` the truth of the593relation symbol `r` on the arguments `xs`. A function symbol enters through its graph. -/594structure FinStr where595  m : Nat596  rel : Nat → List Nat → Bool597598/-- First-order formulas over a relational signature: the atoms `R_r(x_{i₁}, …)` and `x_i = x_j` (variables as de599Bruijn indices), negation, conjunction and the quantifier `∀`, which binds variable `0`. -/600inductive FForm where601  | rel : Nat → List Nat → FForm602  | eq : Nat → Nat → FForm603  | neg : FForm → FForm604  | conj : FForm → FForm → FForm605  | all : FForm → FForm606607/-- Satisfaction, the standard semantics: the quantifier ranges over the structure's elements. -/608def Sat (M : FinStr) : (Nat → Nat) → FForm → Prop609  | env, .rel r xs => M.rel r (xs.map env) = true610  | env, .eq i j => env i = env j611  | env, .neg φ => ¬ Sat M env φ612  | env, .conj φ ψ => Sat M env φ ∧ Sat M env ψ613  | env, .all φ => ∀ x, x < M.m → Sat M (cons x env) φ614615/-- Exhaustive evaluation: each quantifier tries the `m` elements. -/616def fval (M : FinStr) : (Nat → Nat) → FForm → Bool617  | env, .rel r xs => M.rel r (xs.map env)618  | env, .eq i j => decide (env i = env j)619  | env, .neg φ => !(fval M env φ)620  | env, .conj φ ψ => fval M env φ && fval M env ψ621  | env, .all φ => allBelow (fun x => fval M (cons x env) φ) M.m622623theorem allBelow_iff (f : Nat → Bool) : ∀ n, allBelow f n = true ↔ ∀ x, x < n → f x = true624  | 0 => ⟨fun _ _ h => absurd h (Nat.not_lt_zero _), fun _ => rfl⟩625  | n + 1 => by626    show (f n && allBelow f n) = true ↔ _627    have ih := allBelow_iff f n628    match hf : f n with629    | true => exact ⟨fun h x hx => match Nat.lt_or_ge x n with630        | .inl hlt => ih.1 h x hlt631        | .inr hge => (Nat.le_antisymm (Nat.le_of_lt_succ hx) hge) ▸ hf,632        fun h => ih.2 (fun x hx => h x (Nat.lt_succ_of_lt hx))⟩633    | false => exact ⟨fun h => Bool.noConfusion h, fun h => Bool.noConfusion (hf ▸ h n (Nat.lt_succ_self n))⟩634635/-- 25:C2, Z1, 29:B4, 29:E2 — decidable by exhaustive evaluation: a formula holds in the finite structure exactly when its636evaluation is `true`. -/637theorem fin_theory_decidable (M : FinStr) : ∀ (φ : FForm) (env : Nat → Nat), fval M env φ = true ↔ Sat M env φ638  | .rel _ _, _ => Iff.rfl639  | .eq i j, env => show decide (env i = env j) = true ↔ env i = env j from ⟨of_decide_eq_true, decide_eq_true⟩640  | .neg φ, env => by641    show (!(fval M env φ)) = true ↔ ¬ Sat M env φ642    have ih := fin_theory_decidable M φ env643    match h : fval M env φ with644    | true => exact ⟨fun e => Bool.noConfusion e, fun hn => absurd (ih.1 h) hn⟩645    | false => exact ⟨fun _ hs => Bool.noConfusion (h ▸ ih.2 hs), fun _ => rfl⟩646  | .conj φ ψ, env => by647    show (fval M env φ && fval M env ψ) = true ↔ Sat M env φ ∧ Sat M env ψ648    have i1 := fin_theory_decidable M φ env649    have i2 := fin_theory_decidable M ψ env650    match h1 : fval M env φ, h2 : fval M env ψ with651    | true, true => exact ⟨fun _ => ⟨i1.1 h1, i2.1 h2⟩, fun _ => rfl⟩652    | true, false => exact ⟨fun e => Bool.noConfusion e, fun hs => Bool.noConfusion (h2 ▸ i2.2 hs.2)⟩653    | false, _ => exact ⟨fun e => Bool.noConfusion e, fun hs => Bool.noConfusion (h1 ▸ i1.2 hs.1)⟩654  | .all φ, env => by655    show allBelow (fun x => fval M (cons x env) φ) M.m = true ↔ ∀ x, x < M.m → Sat M (cons x env) φ656    exact (allBelow_iff _ M.m).trans ⟨fun h x hx => (fin_theory_decidable M φ (cons x env)).1 (h x hx),657      fun h x hx => (fin_theory_decidable M φ (cons x env)).2 (h x hx)⟩658659/-- 25:C2, Z1, 29:B4 — the theory is complete: every formula or its negation holds, decided by the evaluation, with no660appeal to excluded middle. -/661theorem fin_theory_complete (M : FinStr) (φ : FForm) (env : Nat → Nat) : Sat M env φ ∨ Sat M env (.neg φ) :=662  match h : fval M env φ with663  | true => .inl ((fin_theory_decidable M φ env).1 h)664  | false => .inr (fun hs => Bool.noConfusion (h ▸ (fin_theory_decidable M φ env).2 hs))665666/-- 25:C2, 25:C3, Z1 — the theory is consistent: no formula holds together with its negation. -/667theorem fin_theory_consistent (M : FinStr) (φ : FForm) (env : Nat → Nat) : ¬ (Sat M env φ ∧ Sat M env (.neg φ)) :=668  fun h => h.2 h.1669670/-! ### 00:Z1 — no finite structure interprets Robinson's `Q` -/671672/-- The successor an interpretation defines: on the domain `D`, the least `y` in `D` with `Sg x y`; the identity off it. -/673def succOf (D : Nat → Bool) (Sg : Nat → Nat → Bool) (n x : Nat) : Nat :=674  if D x then (match leastBelow (fun y => D y && Sg x y) n with | some y => y | none => x) else x675676theorem band_l {a b : Bool} (h : (a && b) = true) : a = true := by cases a <;> cases b <;> first | rfl | exact h677theorem band_r {a b : Bool} (h : (a && b) = true) : b = true := by cases a <;> cases b <;> first | rfl | exact h678679/-- 00:Z1, 25:C1 — no finite structure carries Robinson's successor: on `[0, n)`, a domain `D`, a successor relation680`Sg` total on `D`, injective (Q2) and never reaching a zero `Z` of `D` (Q1) cannot exist. A `k`-dimensional681interpretation is the case `n = mᵏ`, its tuples coded below `mᵏ`. -/682theorem no_finite_Q (n : Nat) (D Z : Nat → Bool) (Sg : Nat → Nat → Bool)683    (htot : ∀ x, x < n → D x = true → ∃ y, y < n ∧ D y = true ∧ Sg x y = true)684    (hinj : ∀ x x' y, x < n → x' < n → D x = true → D x' = true → Sg x y = true → Sg x' y = true → x = x')685    (hz : ∃ z, z < n ∧ D z = true ∧ Z z = true)686    (h1 : ∀ x y, x < n → y < n → D x = true → D y = true → Sg x y = true → Z y = false) : False := by687  have hS : ∀ x, x < n → D x = true →688      ∃ y, y < n ∧ D y = true ∧ Sg x y = true ∧ succOf D Sg n x = y := fun x hx hD => by689    obtain ⟨y, hy, hDy, hSy⟩ := htot x hx hD690    obtain ⟨y0, h0⟩ := leastBelow_some (fun y => D y && Sg x y) n y hy (by rw [hDy, hSy]; rfl)691    have sp := leastBelow_spec _ n y0 h0692    refine ⟨y0, sp.1, band_l sp.2.1, band_r sp.2.1, ?_⟩693    show (if D x = true then (match leastBelow (fun y => D y && Sg x y) n with | some y => y | none => x) else x) = y0694    rw [ite_eq_left hD, h0]695  have hoff : ∀ x, D x = false → succOf D Sg n x = x := fun x hD => by696    show (if D x = true then _ else x) = x697    rw [hD, ite_eq_right Bool.false_ne_true]698  obtain ⟨z, hzn, hDz, hZz⟩ := hz699  refine no_finite_successor n (succOf D Sg n) (fun x hx => ?_) (fun x x' hx hx' e => ?_) z hzn (fun x hx e => ?_)700  · match hD : D x with701    | true => obtain ⟨y, hy, _, _, ey⟩ := hS x hx hD; rw [ey]; exact hy702    | false => rw [hoff x hD]; exact hx703  · match hD : D x, hD' : D x' with704    | true, true =>705      obtain ⟨y, _, _, hSy, ey⟩ := hS x hx hD706      obtain ⟨y', _, _, hSy', ey'⟩ := hS x' hx' hD'707      rw [ey, ey'] at e708      exact hinj x x' y hx hx' hD hD' hSy (e ▸ hSy')709    | true, false =>710      obtain ⟨y, _, hDy, _, ey⟩ := hS x hx hD711      rw [ey, hoff x' hD'] at e712      rw [e] at hDy; rw [hDy] at hD'; exact Bool.noConfusion hD'713    | false, true =>714      obtain ⟨y', _, hDy', _, ey'⟩ := hS x' hx' hD'715      rw [ey', hoff x hD] at e716      rw [← e] at hDy'; rw [hDy'] at hD; exact Bool.noConfusion hD717    | false, false => rw [hoff x hD, hoff x' hD'] at e; exact e718  · match hD : D x with719    | true =>720      obtain ⟨y, hy, hDy, hSy, ey⟩ := hS x hx hD721      rw [ey] at e722      have := h1 x y hx hy hD hDy hSy723      rw [e, hZz] at this; exact Bool.noConfusion this724    | false => rw [hoff x hD] at e; rw [e, hDz] at hD; exact Bool.noConfusion hD725726/-- 00:Z1, 25:C1 — a finite structure interprets no Robinson `Q`: for formulas `δ` (the domain, in variable `0`),727`σ` (the successor's graph, `x` in variable `1` and `y` in `0`) and `ζ` (zero), the relativised successor axioms —728`S` total on the domain, Q2 (`S x = S x' → x = x'`), a zero in the domain, and Q1 (`S x ≠ 0`) — never all hold. -/729theorem no_interpretation (M : FinStr) (env : Nat → Nat) (δ σ ζ : FForm) :730    ¬ ((∀ x, x < M.m → Sat M (cons x env) δ →731        ∃ y, y < M.m ∧ Sat M (cons y env) δ ∧ Sat M (cons y (cons x env)) σ) ∧732      (∀ x x' y, x < M.m → x' < M.m → Sat M (cons x env) δ → Sat M (cons x' env) δ →733        Sat M (cons y (cons x env)) σ → Sat M (cons y (cons x' env)) σ → x = x') ∧734      (∃ z, z < M.m ∧ Sat M (cons z env) δ ∧ Sat M (cons z env) ζ) ∧735      (∀ x y, x < M.m → y < M.m → Sat M (cons x env) δ → Sat M (cons y env) δ → Sat M (cons y (cons x env)) σ →736        ¬ Sat M (cons y env) ζ)) := fun ⟨htot, hinj, ⟨z, hz, hDz, hZz⟩, h1⟩ => by737  have dec := fin_theory_decidable M738  refine no_finite_Q M.m (fun x => fval M (cons x env) δ) (fun x => fval M (cons x env) ζ)739    (fun x y => fval M (cons y (cons x env)) σ) (fun x hx hD => ?_) (fun x x' y hx hx' hD hD' hS hS' => ?_)740    ⟨z, hz, (dec δ _).2 hDz, (dec ζ _).2 hZz⟩ (fun x y hx hy hD hDy hS => ?_)741  · obtain ⟨y, hy, hDy, hSy⟩ := htot x hx ((dec δ _).1 hD)742    exact ⟨y, hy, (dec δ _).2 hDy, (dec σ _).2 hSy⟩743  · exact hinj x x' y hx hx' ((dec δ _).1 hD) ((dec δ _).1 hD') ((dec σ _).1 hS) ((dec σ _).1 hS')744  · match hZ : fval M (cons y env) ζ with745    | false => rfl746    | true => exact absurd ((dec ζ _).1 hZ) (h1 x y hx hy ((dec δ _).1 hD) ((dec δ _).1 hDy) ((dec σ _).1 hS))747748end FRC.Logic749