Ordinal-valued depth of Lω₁ω formulas

The well-founded measure for quantifier recursions over BoundedFormulaω (extracted from Methods/Henkin/Construction.lean, where it was born as the truthLemma termination measure, and re-derived privately by Methods/Interpolation/QuotientTruthLemma.lean — this neutral home serves both). sizeOf is inadequate: sizeOf (φs k) is unbounded while sizeOf (iSup φs) = 2, and the all case recurses on (φ.openBounds).subst t, not a structural subterm. depth uses Ordinal.iSup at the countable connectives and is preserved by castLE, relabel, openBounds, and subst, with strict decrease into every connective.

Ordinal-valued depth for termination of truthLemma

The standard sizeOf measure is inadequate for truthLemma because:

• sizeOf (fun k => φs k) = 1 for function types, so sizeOf (iSup φs) = 2, yet sizeOf (φs k) can be arbitrarily large.
• The all case recurses on (φ.openBounds).subst t, which is not a structural subterm.

We define an Ordinal-valued depth that uses iSup for iSup/iInf cases, then prove it is preserved by castLE, relabel, openBounds, and subst.

noncomputable def FirstOrder.Language.BoundedFormulaω.depth {L : Language} {α : Type u_1} {n : ℕ} : L.BoundedFormulaω α n → Ordinal.{0}

Ordinal-valued depth of a bounded formula. Uses Ordinal.iSup at iSup/iInf nodes to ensure each component φs k has strictly smaller depth.

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.depth = 0
• (FirstOrder.Language.BoundedFormulaω.equal t₁ t₂).depth = 0
• (FirstOrder.Language.BoundedFormulaω.rel R ts).depth = 0
• (φ.imp ψ).depth = max φ.depth ψ.depth + 1
• φ.all.depth = φ.depth + 1
• (FirstOrder.Language.BoundedFormulaω.iSup φs).depth = (⨆ (k : ℕ), (φs k).depth) + 1
• (FirstOrder.Language.BoundedFormulaω.iInf φs).depth = (⨆ (k : ℕ), (φs k).depth) + 1

theorem FirstOrder.Language.depth_lt_imp_left {L : Language} {α : Type u_1} {n : ℕ} {φ ψ : L.BoundedFormulaω α n} : φ.depth < (φ.imp ψ).depth

theorem FirstOrder.Language.depth_lt_imp_right {L : Language} {α : Type u_1} {n : ℕ} {φ ψ : L.BoundedFormulaω α n} : ψ.depth < (φ.imp ψ).depth

theorem FirstOrder.Language.depth_lt_iSup {L : Language} {α : Type u_1} {n : ℕ} {φs : ℕ → L.BoundedFormulaω α n} (k : ℕ) : (φs k).depth < (BoundedFormulaω.iSup φs).depth

theorem FirstOrder.Language.depth_lt_iInf {L : Language} {α : Type u_1} {n : ℕ} {φs : ℕ → L.BoundedFormulaω α n} (k : ℕ) : (φs k).depth < (BoundedFormulaω.iInf φs).depth

theorem FirstOrder.Language.depth_lt_all {L : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormulaω α (n + 1)} : φ.depth < φ.all.depth

theorem FirstOrder.Language.depth_castLE {L : Language} {m n : ℕ} {α : Type u_1} (h : m ≤ n) (φ : L.BoundedFormulaω α m) : (BoundedFormulaω.castLE h φ).depth = φ.depth

theorem FirstOrder.Language.depth_relabel {L : Language} {α β : Type u_1} {p n : ℕ} (g : α → β ⊕ Fin p) (φ : L.BoundedFormulaω α n) : (BoundedFormulaω.relabel g φ).depth = φ.depth

theorem FirstOrder.Language.depth_openBounds {L : Language} {n : ℕ} (φ : L.BoundedFormulaω Empty n) : BoundedFormulaω.depth φ.openBounds = φ.depth

theorem FirstOrder.Language.depth_subst {L : Language} {α : Type u_1} {n : ℕ} {β : Type u_1} (φ : L.BoundedFormulaω α n) (tf : α → L.Term β) : (φ.subst tf).depth = φ.depth

theorem FirstOrder.Language.depth_openBounds_subst_lt {L : Language} {n : ℕ} {β : Type} {φ : L.BoundedFormulaω Empty (n + 1)} (tf : Fin (n + 1) → L.Term β) : (BoundedFormulaω.subst φ.openBounds tf).depth < φ.all.depth

depth (openBounds φ).subst t < depth (all φ) for the truthLemma termination proof.