Theme/SecondOrder.lean — FrcCore

1import FrcCore.Theme.Logic23/-!4# The full second-order theory of a finite structure (the logic theme; 29-finitism, 9 October 2026)56A finite relational structure `FinStr` (`Theme/Logic.lean`) has finitely many subsets and finitely many relations of7each arity. A subset of its `m` elements is coded by a number below `2^m` (bit `x` for element `x`), and a relation of8arity `a` by a number below `2^(m^a)` (one bit per tuple, the tuple coded in base `m`). Second-order formulas add set9and relation variables, their atoms and their quantifiers to the first-order formulas; satisfaction ranges over the10codes, and exhaustive evaluation tries them all. `so_theory_decidable` is the second-order form of11`fin_theory_decidable`: the full second-order theory of a finite structure is decided by evaluation (29-finitism,12Corollary determinacy, the finite direction; 5-reductio D8). No axioms.13-/1415namespace FRC.Logic1617/-- Bit `x` of the code `n`: whether element `x` belongs to the subset coded by `n`. -/18def memBit (n x : Nat) : Bool := decide (n / 2 ^ x % 2 = 1)1920/-- The code of a tuple of elements in base `m`: `x₀ + m x₁ + m² x₂ + …`. -/21def tupleIndex (m : Nat) : List Nat → Nat22  | [] => 023  | x :: xs => x + m * tupleIndex m xs2425/-- Second-order formulas: the first-order atoms, the set atom `X_k(x_i)`, the relation atom `R_k(x_{i₁}, …)`,26negation, conjunction, and the three quantifiers — over elements, over subsets (binding set variable `0`), over27relations of arity `a` (binding relation variable `0`). Variables are de Bruijn indices in three sorts. -/28inductive SForm where29  | rel : Nat → List Nat → SForm30  | eq : Nat → Nat → SForm31  | setMem : Nat → Nat → SForm32  | relApp : Nat → List Nat → SForm33  | neg : SForm → SForm34  | conj : SForm → SForm → SForm35  | all : SForm → SForm36  | allSet : SForm → SForm37  | allRel : Nat → SForm → SForm3839/-- Satisfaction: the element quantifier ranges over the `m` elements, the set quantifier over the `2^m` codes of40subsets, the relation quantifier of arity `a` over the `2^(m^a)` codes of relations. -/41def Sat2 (M : FinStr) : (Nat → Nat) → (Nat → Nat) → (Nat → Nat) → SForm → Prop42  | env, _, _, .rel r xs => M.rel r (xs.map env) = true43  | env, _, _, .eq i j => env i = env j44  | env, senv, _, .setMem k i => memBit (senv k) (env i) = true45  | env, _, renv, .relApp k xs => memBit (renv k) (tupleIndex M.m (xs.map env)) = true46  | env, senv, renv, .neg φ => ¬ Sat2 M env senv renv φ47  | env, senv, renv, .conj φ ψ => Sat2 M env senv renv φ ∧ Sat2 M env senv renv ψ48  | env, senv, renv, .all φ => ∀ x, x < M.m → Sat2 M (cons x env) senv renv φ49  | env, senv, renv, .allSet φ => ∀ S, S < 2 ^ M.m → Sat2 M env (cons S senv) renv φ50  | env, senv, renv, .allRel a φ => ∀ R, R < 2 ^ (M.m ^ a) → Sat2 M env senv (cons R renv) φ5152/-- Exhaustive evaluation: each quantifier tries every code below its bound. -/53def sval2 (M : FinStr) : (Nat → Nat) → (Nat → Nat) → (Nat → Nat) → SForm → Bool54  | env, _, _, .rel r xs => M.rel r (xs.map env)55  | env, _, _, .eq i j => decide (env i = env j)56  | env, senv, _, .setMem k i => memBit (senv k) (env i)57  | env, _, renv, .relApp k xs => memBit (renv k) (tupleIndex M.m (xs.map env))58  | env, senv, renv, .neg φ => !(sval2 M env senv renv φ)59  | env, senv, renv, .conj φ ψ => sval2 M env senv renv φ && sval2 M env senv renv ψ60  | env, senv, renv, .all φ => allBelow (fun x => sval2 M (cons x env) senv renv φ) M.m61  | env, senv, renv, .allSet φ => allBelow (fun S => sval2 M env (cons S senv) renv φ) (2 ^ M.m)62  | env, senv, renv, .allRel a φ => allBelow (fun R => sval2 M env senv (cons R renv) φ) (2 ^ (M.m ^ a))6364/-- 29:E4 — Corollary determinacy, the finite direction (5:D8): the full second-order theory of a finite structure is65decided by exhaustive evaluation, a formula holds exactly when its evaluation is `true`. -/66theorem so_theory_decidable (M : FinStr) : ∀ (φ : SForm) (env senv renv : Nat → Nat),67    sval2 M env senv renv φ = true ↔ Sat2 M env senv renv φ68  | .rel _ _, _, _, _ => Iff.rfl69  | .eq i j, env, _, _ => show decide (env i = env j) = true ↔ env i = env j from ⟨of_decide_eq_true, decide_eq_true⟩70  | .setMem _ _, _, _, _ => Iff.rfl71  | .relApp _ _, _, _, _ => Iff.rfl72  | .neg φ, env, senv, renv => by73    show (!(sval2 M env senv renv φ)) = true ↔ ¬ Sat2 M env senv renv φ74    have ih := so_theory_decidable M φ env senv renv75    match h : sval2 M env senv renv φ with76    | true => exact ⟨fun e => Bool.noConfusion e, fun hn => absurd (ih.1 h) hn⟩77    | false => exact ⟨fun _ hs => Bool.noConfusion (h ▸ ih.2 hs), fun _ => rfl⟩78  | .conj φ ψ, env, senv, renv => by79    show (sval2 M env senv renv φ && sval2 M env senv renv ψ) = true ↔ Sat2 M env senv renv φ ∧ Sat2 M env senv renv ψ80    have i1 := so_theory_decidable M φ env senv renv81    have i2 := so_theory_decidable M ψ env senv renv82    match h1 : sval2 M env senv renv φ, h2 : sval2 M env senv renv ψ with83    | true, true => exact ⟨fun _ => ⟨i1.1 h1, i2.1 h2⟩, fun _ => rfl⟩84    | true, false => exact ⟨fun e => Bool.noConfusion e, fun hs => Bool.noConfusion (h2 ▸ i2.2 hs.2)⟩85    | false, _ => exact ⟨fun e => Bool.noConfusion e, fun hs => Bool.noConfusion (h1 ▸ i1.2 hs.1)⟩86  | .all φ, env, senv, renv => by87    show allBelow (fun x => sval2 M (cons x env) senv renv φ) M.m = true ↔ ∀ x, x < M.m → Sat2 M (cons x env) senv renv φ88    exact (allBelow_iff _ M.m).trans ⟨fun h x hx => (so_theory_decidable M φ (cons x env) senv renv).1 (h x hx),89      fun h x hx => (so_theory_decidable M φ (cons x env) senv renv).2 (h x hx)⟩90  | .allSet φ, env, senv, renv => by91    show allBelow (fun S => sval2 M env (cons S senv) renv φ) (2 ^ M.m) = true ↔92      ∀ S, S < 2 ^ M.m → Sat2 M env (cons S senv) renv φ93    exact (allBelow_iff _ (2 ^ M.m)).trans ⟨fun h S hS => (so_theory_decidable M φ env (cons S senv) renv).1 (h S hS),94      fun h S hS => (so_theory_decidable M φ env (cons S senv) renv).2 (h S hS)⟩95  | .allRel a φ, env, senv, renv => by96    show allBelow (fun R => sval2 M env senv (cons R renv) φ) (2 ^ (M.m ^ a)) = true ↔97      ∀ R, R < 2 ^ (M.m ^ a) → Sat2 M env senv (cons R renv) φ98    exact (allBelow_iff _ (2 ^ (M.m ^ a))).trans ⟨fun h R hR => (so_theory_decidable M φ env senv (cons R renv)).1 (h R hR),99      fun h R hR => (so_theory_decidable M φ env senv (cons R renv)).2 (h R hR)⟩100101/-- 29:E4 — Corollary determinacy, the finite direction: the full second-order theory is complete, every formula or its102negation holds, decided by the evaluation. -/103theorem so_theory_complete (M : FinStr) (φ : SForm) (env senv renv : Nat → Nat) :104    Sat2 M env senv renv φ ∨ Sat2 M env senv renv (.neg φ) :=105  match h : sval2 M env senv renv φ with106  | true => .inl ((so_theory_decidable M φ env senv renv).1 h)107  | false => .inr (fun hs => Bool.noConfusion (h ▸ (so_theory_decidable M φ env senv renv).2 hs))108109/-- 29:E4 — the full second-order theory is consistent: no formula holds together with its negation. -/110theorem so_theory_consistent (M : FinStr) (φ : SForm) (env senv renv : Nat → Nat) :111    ¬ (Sat2 M env senv renv φ ∧ Sat2 M env senv renv (.neg φ)) :=112  fun h => h.2 h.1113114/-- The subsets of `m` elements are `2^m` codes and the relations of arity `a` are `2^(m^a)`: both finite, and every115code below the bound is a subset or a relation (every bit pattern is one). The quantifiers of `Sat2` range over exactly116these, so the evaluation is uniform in the structure: `sval2` is a terminating computation on `M` presented as data. -/117theorem so_evaluation_terminates (M : FinStr) (φ : SForm) (env senv renv : Nat → Nat) :118    sval2 M env senv renv φ = true ∨ sval2 M env senv renv φ = false :=119  match sval2 M env senv renv φ with120  | true => .inl rfl121  | false => .inr rfl122123end FRC.Logic124