Change bootstrapping 2

Foundation.lean

@@ -53,7 +53,6 @@ public import Foundation.FirstOrder.Basic.Semantics.Semantics
 public import Foundation.FirstOrder.Basic.Soundness
 public import Foundation.FirstOrder.Basic.Syntax.Formula
 public import Foundation.FirstOrder.Basic.Syntax.Rew
-public import Foundation.FirstOrder.Basic.Syntax.Schema
 -- public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D1
 -- public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D2
 -- public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3
@@ -75,8 +74,9 @@ public import Foundation.FirstOrder.Basic.Syntax.Schema
 -- public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions
 -- public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed
 -- public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory
-public import Foundation.FirstOrder.Completeness.BooleanValuedModel
 public import Foundation.FirstOrder.Completeness.CanonicalModel
+public import Foundation.FirstOrder.Completeness.CountableSublanguage
+public import Foundation.FirstOrder.Completeness.CounterModel
 -- public import Foundation.FirstOrder.Hauptsatz
 -- public import Foundation.FirstOrder.Incompleteness.Consistency
 -- public import Foundation.FirstOrder.Incompleteness.Dense
@@ -116,7 +116,7 @@ public import Foundation.FirstOrder.Polarity
 -- public import Foundation.FirstOrder.SetTheory.TransitiveModel
 -- public import Foundation.FirstOrder.SetTheory.Universe
 -- public import Foundation.FirstOrder.SetTheory.Z
-public import Foundation.FirstOrder.Skolemization.Hull
+-- public import Foundation.FirstOrder.Skolemization.Hull
 public import Foundation.FirstOrder.Ultraproduct
 public import Foundation.Init
 public import Foundation.InterpretabilityLogic.Axioms
@@ -375,7 +375,7 @@ public import Foundation.Modal.VanBentham.StandardTranslation
 public import Foundation.Propositional.Boolean.Basic
 public import Foundation.Propositional.Boolean.Hilbert
 public import Foundation.Propositional.Boolean.NNFormula
-public import Foundation.Propositional.Boolean.Tait
+-- public import Foundation.Propositional.Boolean.Tait
 public import Foundation.Propositional.Boolean.ZeroSubst
 public import Foundation.Propositional.ConsistentTableau
 public import Foundation.Propositional.Dialectica.Basic
@@ -458,7 +458,7 @@ public import Foundation.Propositional.Neighborhood.NB.Basic
 public import Foundation.Propositional.Neighborhood.NB.Hilbert.Basic
 public import Foundation.Propositional.Neighborhood.NB.Hilbert.WF
 public import Foundation.Propositional.Slash
-public import Foundation.Propositional.Tait.Calculus
+-- public import Foundation.Propositional.Tait.Calculus
 public import Foundation.Propositional.Translation
 -- public import Foundation.ProvabilityLogic.Arithmetic
 -- public import Foundation.ProvabilityLogic.Classification.LetterlessTrace

Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean

@@ -256,7 +256,7 @@ lemma sigma_of_sigma_ex {φ : Semiformula L ξ (n + 1)} : Hierarchy 𝚺 s (∃
 
 set_option linter.flexible false in
 lemma rew (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : Hierarchy Γ s φ → Hierarchy Γ s (ω ▹ φ) := by
-  intro h; induction h generalizing n₂ <;> try simp [*, Semiformula.rew_rel, Semiformula.rew_nrel]
+  intro h; induction h generalizing n₂ <;> try simp [*]
   case sigma ih => exact (ih _).accum _
   case pi ih => exact (ih _).accum _
   case dummy_pi ih => exact (ih _).dummy_pi
@@ -476,7 +476,7 @@ end Arithmetic
 abbrev ArithmeticTheory.SoundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) := T.SoundOn (Arithmetic.Hierarchy Γ k)
 
 lemma ArithmeticTheory.soundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) [T.SoundOnHierarchy Γ k] :
-    T ⊢ σ → Arithmetic.Hierarchy Γ k σ → ℕ ⊧ₘ σ := SoundOn.sound
+    T ⊢ σ → Arithmetic.Hierarchy Γ k σ → ℕ↓[ℒₒᵣ] ⊧ σ := SoundOn.sound
 
 instance (T : ArithmeticTheory) [T.SoundOnHierarchy 𝚺 1] : Entailment.Consistent T :=
   T.consistent_of_sound (Arithmetic.Hierarchy 𝚺 1) (by simp)

Foundation/FirstOrder/Arithmetic/Basic/Misc.lean

@@ -135,14 +135,12 @@ def bexsLTSucc (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformu
 
 variable {M : Type*} {s : Structure L M} [LT M] [One M] [Add M] [Structure.LT L M] [Structure.One L M] [Structure.Add L M]
 
-variable {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)}
-
-lemma eval_ballLTSucc {e ε} :
-    Eval s e ε (φ.ballLTSucc t) ↔ ∀ x < t.val s e ε + 1, Eval s (x :> e) ε φ := by
+lemma eval_ballLTSucc {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv bv} :
+    (φ.ballLTSucc t).Eval (M := M) fv bv ↔ ∀ x < t.val (M := M) fv bv + 1, φ.Eval (M := M) (x :> fv) bv := by
   simp [ballLTSucc, Semiterm.Operator.numeral]
 
-lemma eval_bexsLTSucc {e ε} :
-    Eval s e ε (φ.bexsLTSucc t) ↔ ∃ x < t.val s e ε + 1, Eval s (x :> e) ε φ := by
+lemma eval_bexsLTSucc {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv bv} :
+    (φ.bexsLTSucc t).Eval (M := M) fv bv ↔ ∃ x < t.val (M := M) fv bv + 1, φ.Eval (M := M) (x :> fv) bv := by
   simp [bexsLTSucc, Semiterm.Operator.numeral]
 
 end Semiformula
@@ -167,8 +165,6 @@ macro_rules
 
 end BinderNotation
 
-abbrev ArithmeticTheory := Theory ℒₒᵣ
-
 end FirstOrder
 
 end LO

Foundation/FirstOrder/Arithmetic/Basic/Model.lean

@@ -5,15 +5,15 @@ public import Foundation.FirstOrder.Arithmetic.Basic.Misc
 @[expose] public section
 namespace LO.FirstOrder.Arithmetic
 
-private lemma consequence_of_aux (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ)
+private lemma complete_aux (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Sentence ℒₒᵣ)
     (H : ∀ (M : Type w)
            [ORingStructure M]
            [Structure ℒₒᵣ M]
            [Structure.ORing ℒₒᵣ M]
-           [M ⊧ₘ* T],
-           M ⊧ₘ φ) :
-    T ⊨ φ := consequence_iff_consequence.{_, w}.mp <| consequence_iff_eq.mpr fun M _ _ _ hT =>
-  letI : Structure.Model ℒₒᵣ M ⊧ₘ* T := Structure.ElementaryEquiv.modelsTheory.mp hT
+           [M↓[ℒₒᵣ] ⊧* T],
+           M↓[ℒₒᵣ] ⊧ φ) :
+    T ⊢ φ := Theory.Proof.complete <| consequence_iff_eq.mpr fun M _ _ _ hT ↦
+  letI : (Structure.Model ℒₒᵣ M)↓[ℒₒᵣ] ⊧* T := Structure.ElementaryEquiv.modelsTheory.mp hT
   Structure.ElementaryEquiv.models.mpr (H (Structure.Model ℒₒᵣ M))
 
 open Language
@@ -23,38 +23,40 @@ section semantics
 variable (M : Type*) [ORingStructure M]
 
 instance standardModel : Structure ℒₒᵣ M where
-  func := fun _ f =>
+  func := fun _ f ↦
     match f with
-    | ORing.Func.zero => fun _ => 0
-    |  ORing.Func.one => fun _ => 1
-    |  ORing.Func.add => fun v => v 0 + v 1
-    |  ORing.Func.mul => fun v => v 0 * v 1
-  rel := fun _ r =>
+    | ORing.Func.zero => fun _ ↦ 0
+    |  ORing.Func.one => fun _ ↦ 1
+    |  ORing.Func.add => fun v ↦ v 0 + v 1
+    |  ORing.Func.mul => fun v ↦ v 0 * v 1
+  rel := fun _ r ↦
     match r with
-    | ORing.Rel.eq => fun v => v 0 = v 1
-    | ORing.Rel.lt => fun v => v 0 < v 1
+    | ORing.Rel.eq => fun v ↦ v 0 = v 1
+    | ORing.Rel.lt => fun v ↦ v 0 < v 1
 
-instance : Structure.Eq ℒₒᵣ M :=
-  ⟨by intro a b; simp [standardModel, Semiformula.Operator.val, Semiformula.Operator.Eq.sentence_eq, Semiformula.eval_rel]⟩
+instance : Structure.Eq ℒₒᵣ M where
+  eq a b := by
+    unfold standardModel
+    simp [Semiformula.Operator.val, Semiformula.Operator.Eq.sentence_eq]
 
 instance : Structure.Zero ℒₒᵣ M := ⟨rfl⟩
 
 instance : Structure.One ℒₒᵣ M := ⟨rfl⟩
 
-instance : Structure.Add ℒₒᵣ M := ⟨fun _ _ => rfl⟩
+instance : Structure.Add ℒₒᵣ M := ⟨fun _ _ ↦ rfl⟩
 
-instance : Structure.Mul ℒₒᵣ M := ⟨fun _ _ => rfl⟩
+instance : Structure.Mul ℒₒᵣ M := ⟨fun _ _ ↦ rfl⟩
 
-instance : Structure.Eq ℒₒᵣ M := ⟨fun _ _ => iff_of_eq rfl⟩
+instance : Structure.Eq ℒₒᵣ M := ⟨fun _ _ ↦ iff_of_eq rfl⟩
 
-instance : Structure.LT ℒₒᵣ M := ⟨fun _ _ => iff_of_eq rfl⟩
+instance : Structure.LT ℒₒᵣ M := ⟨fun _ _ ↦ iff_of_eq rfl⟩
 
 instance : ORing ℒₒᵣ := ORing.mk
 
 lemma standardModel_unique' (s : Structure ℒₒᵣ M)
     (hZero : Structure.Zero ℒₒᵣ M) (hOne : Structure.One ℒₒᵣ M) (hAdd : Structure.Add ℒₒᵣ M) (hMul : Structure.Mul ℒₒᵣ M)
     (hEq : Structure.Eq ℒₒᵣ M) (hLT : Structure.LT ℒₒᵣ M) : s = standardModel M := Structure.ext
-  (funext₃ fun k f _ =>
+  (funext₃ fun k f _ ↦
     match k, f with
     | _, Language.Zero.zero => by simp [Matrix.empty_eq]
     | _,   Language.One.one => by simp [Matrix.empty_eq]
@@ -72,31 +74,29 @@ lemma standardModel_unique (s : Structure ℒₒᵣ M)
 
 end semantics
 
-lemma consequence_of_models (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M ⊧ₘ* T], M ⊧ₘ φ) :
-    T ⊨ φ := consequence_of_aux T φ fun M _ s _ _ ↦ by
+/-- provable_of_models -/
+lemma complete (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M↓[ℒₒᵣ] ⊧* T], M↓[ℒₒᵣ] ⊧ φ) :
+    T ⊢ φ := complete_aux T φ fun M _ s _ _ ↦ by
   rcases standardModel_unique M s
   exact H M
 
-lemma provable_of_models (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M ⊧ₘ* T], M ⊧ₘ φ) :
-    T ⊢ φ := complete <| consequence_of_models _ _ H
-
-lemma weakerThan_of_models (T S : ArithmeticTheory) [𝗘𝗤 ⪯ S]
+lemma weakerThan_of_models (T S : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ S]
     (H : ∀ (M : Type*)
            [ORingStructure M]
-           [M ⊧ₘ* S],
-           M ⊧ₘ* T) : T ⪯ S :=
-  Entailment.weakerThan_iff.mpr fun h ↦ complete <| consequence_of_models _ _ fun M _ _ ↦ sound! h (H M)
+           [M↓[ℒₒᵣ] ⊧* S],
+           M↓[ℒₒᵣ] ⊧* T) : T ⪯ S :=
+  Entailment.weakerThan_iff.mpr fun h ↦ complete _ _ fun M _ _ ↦ Theory.Proof.sound h (H M)
 
 end Arithmetic
 
 class ArithmeticTheory.SoundOn (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop) where
-  sound : ∀ {σ}, T ⊢ σ → F σ → ℕ ⊧ₘ σ
+  sound : ∀ {σ}, T ⊢ σ → F σ → ℕ↓[ℒₒᵣ] ⊧ σ
 
 namespace ArithmeticTheory
 
 variable (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop)
 
-instance [ℕ ⊧ₘ* T] : T.SoundOn F := ⟨fun b _ ↦ consequence_iff.mp (sound! b) ℕ inferInstance⟩
+instance [ℕ↓[ℒₒᵣ] ⊧* T] : T.SoundOn F := ⟨fun b _ ↦ consequence_iff.mp (Theory.Proof.sound b) ℕ inferInstance⟩
 
 lemma consistent_of_sound [SoundOn T F] (hF : F ⊥) : Entailment.Consistent T :=
   Entailment.consistent_iff_unprovable_bot.mpr fun b ↦ SoundOn.sound b hF

Foundation/FirstOrder/Arithmetic/Basic/Monotone.lean

@@ -14,9 +14,9 @@ namespace Monotone
 
 variable {L : Language} {M : Type*} [LE M] [Structure L M] [Monotone L M]
 
-lemma term_monotone (t : Semiterm L ξ n) {e₁ e₂ : Fin n → M} {ε₁ ε₂ : ξ → M}
-    (he : ∀ i, e₁ i ≤ e₂ i) (hε : ∀ i, ε₁ i ≤ ε₂ i) :
-    t.valm M e₁ ε₁ ≤ t.valm M e₂ ε₂ := by
+lemma term_monotone (t : Semiterm L ξ n) {fv₁ fv₂ : Fin n → M} {bv₁ bv₂ : ξ → M}
+    (he : ∀ i, fv₁ i ≤ fv₂ i) (hε : ∀ i, bv₁ i ≤ bv₂ i) :
+    t.val fv₁ bv₁ ≤ t.val fv₂ bv₂ := by
   induction t <;> simp [*, Semiterm.val_func, Monotone.monotone]
 
 end Monotone

Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean

@@ -8,76 +8,78 @@ namespace LO.FirstOrder.Arithmetic
 open PeanoMinus R0
 
 lemma nat_modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
-    ℕ ⊧/v φ ↔ ℕ ⊧ₘ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
-  simp [models_iff]
+    φ.Evalb v ↔ ℕ↓[ℒₒᵣ] ⊧ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
+  simp [models_iff, Function.comp_def, Matrix.empty_eq]
 
-variable (V : Type*) [ORingStructure V] [V ⊧ₘ* 𝗣𝗔⁻]
+variable (V : Type*) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻]
 
 lemma modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
-    V ⊧/(v ·) φ ↔ V ⊧ₘ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
-  simp [models_iff, numeral_eq_natCast]
+    φ.Evalb (M := V) (Nat.cast ∘ v) ↔ V↓[ℒₒᵣ] ⊧ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
+  simp [models_iff, Function.comp_def, Matrix.empty_eq, numeral_eq_natCast]
 
 lemma shigmaZero_absolute {k} (φ : 𝚺₀.Semisentence k) (v : Fin k → ℕ) :
-    ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
+    φ.val.Evalb v ↔ φ.val.Evalb (M := V) (Nat.cast ∘ v) :=
   ⟨by simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs] using nat_extention_sigmaOne V (by simp),
    by simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs] using nat_extention_piOne V (by simp)⟩
 
 lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k}
     (hR : 𝚺₀.Defined R φ) (hR' : 𝚺₀.Defined R' φ) (v : Fin k → ℕ) :
-    R v ↔ R' (fun i ↦ (v i : V)) := by
+    R v ↔ R' (Nat.cast ∘ v) := by
   simpa [hR.iff, hR'.iff] using Arithmetic.shigmaZero_absolute V φ v
 
 lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1)}
     (hf : 𝚺₀.DefinedFunction f φ) (hf' : 𝚺₀.DefinedFunction f' φ) (v : Fin k → ℕ) :
-    (f v : V) = f' (fun i ↦ (v i)) := by
+    (f v : V) = f' (Nat.cast ∘ v) := by
   simpa using Defined.shigmaZero_absolute V hf hf' (f v :> v)
 
 lemma sigmaOne_upward_absolute {k} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
-    ℕ ⊧/v φ.val → V ⊧/(v ·) φ.val := by
+    φ.val.Evalb v → φ.val.Evalb (M := V) (Nat.cast ∘ v) := by
   simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   using nat_extention_sigmaOne V (by simp)
 
 lemma piOne_downward_absolute {k} (φ : 𝚷₁.Semisentence k) (v : Fin k → ℕ) :
-    V ⊧/(v ·) φ.val → ℕ ⊧/v φ.val := by
+    φ.val.Evalb (M := V) (Nat.cast ∘ v) → φ.val.Evalb v := by
   simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   using nat_extention_piOne V (by simp)
 
 lemma deltaOne_absolute {k} (φ : 𝚫₁.Semisentence k)
     (properNat : φ.ProperOn ℕ) (proper : φ.ProperOn V) (v : Fin k → ℕ) :
-    ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
+    φ.val.Evalb v ↔ φ.val.Evalb (M := V) (Nat.cast ∘ v) :=
   ⟨by simpa [HierarchySymbol.Semiformula.val_sigma] using sigmaOne_upward_absolute V φ.sigma v,
    by simpa [proper.iff', properNat.iff'] using piOne_downward_absolute V φ.pi v⟩
 
 lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚫₁.Semisentence k}
     (hR : 𝚫₁.Defined R φ) (hR' : 𝚫₁.Defined R' φ) (v : Fin k → ℕ) :
-    R v ↔ R' (fun i ↦ (v i : V)) := by
+    R v ↔ R' (Nat.cast ∘ v) := by
   simpa using deltaOne_absolute V φ hR.proper hR'.proper v
 
 lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1)}
     (hf : 𝚺₁.DefinedFunction f φ) (hf' : 𝚺₁.DefinedFunction f' φ) (v : Fin k → ℕ) :
-    (f v : V) = f' (fun i ↦ (v i)) := by
+    (f v : V) = f' (Nat.cast ∘ v) := by
   simpa using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v)
 
 variable {V}
 
 lemma models_iff_of_Sigma0 {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ ↔ ℕ ⊧/e σ := by
-  by_cases h : ℕ ⊧/e σ <;> simp [h]
-  · have : V ⊧/(e ·) σ := by
+    σ.Evalb (M := V) (Nat.cast ∘ e) ↔ σ.Evalb e := by
+  by_cases h : σ.Evalb e <;> simp [h]
+  · have : σ.Evalb (M := V) (Nat.cast ∘ e) := by
       simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) h
     simpa [HierarchySymbol.Semiformula.val_sigma] using this
-  · have : ℕ ⊧/e (∼σ) := by simpa using h
-    have : V ⊧/(e ·) (∼σ) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) this
+  · have : (∼σ).Evalb (M := ℕ) e := by simpa using h
+    have : (∼σ).Evalb (M := V) (Nat.cast ∘ e) := by
+      simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) this
     simpa using this
 
 lemma models_iff_of_Delta1 {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ.val ↔ ℕ ⊧/e σ.val := by
-  by_cases h : ℕ ⊧/e σ.val <;> simp [h]
-  · have : ℕ ⊧/e σ.sigma.val := by simpa [HierarchySymbol.Semiformula.val_sigma] using h
-    have : V ⊧/(e ·) σ.sigma.val := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
+    σ.val.Evalb (M := V) (Nat.cast ∘ e) ↔ σ.val.Evalb e := by
+  by_cases h : σ.val.Evalb e <;> simp [h]
+  · have : σ.sigma.val.Evalb e := by simpa [HierarchySymbol.Semiformula.val_sigma] using h
+    have : σ.sigma.val.Evalb (M := V) (Nat.cast ∘ e) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
     simpa [HierarchySymbol.Semiformula.val_sigma] using this
-  · have : ℕ ⊧/e (∼σ.pi.val) := by simpa [hσ.iff'] using h
-    have : V ⊧/(e ·) (∼σ.pi.val) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
+  · have : (∼σ.pi.val).Evalb (M := ℕ) e := by simpa [hσ.iff'] using h
+    have : (∼σ.pi.val).Evalb (M := V) (Nat.cast ∘ e) := by
+      simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
     simpa [hσV.iff'] using this
 
 variable {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] [T.SoundOnHierarchy 𝚺 1]
@@ -86,21 +88,21 @@ noncomputable instance : 𝗥₀ ⪯ T := Entailment.WeakerThan.trans (𝓣 := 
 
 theorem sigma_one_completeness_iff_param {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} :
     ℕ ⊧/e σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := Iff.trans
-  (by simp [models_iff, Semiformula.eval_substs])
+  (by simp [models_iff, Semiformula.eval_substs, Function.comp_def, Matrix.empty_eq])
   (sigma_one_completeness_iff (T := T) (by simp [hσ]))
 
-lemma models_iff_provable_of_Sigma0_param [V ⊧ₘ* T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
+lemma models_iff_provable_of_Sigma0_param [V↓[ℒₒᵣ] ⊧* T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
+    V ⊧/(Nat.cast ∘ e) σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
   calc
-    V ⊧/(e ·) σ ↔ ℕ ⊧/e σ        := by
+    V ⊧/(Nat.cast ∘ e) σ ↔ ℕ ⊧/e σ        := by
       simp [models_iff_of_Sigma0 hσ]
   _             ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
       apply sigma_one_completeness_iff_param (by simp [Hierarchy.of_zero hσ])
 
-lemma models_iff_provable_of_Delta1_param [V ⊧ₘ* T] {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ.val ↔ T ⊢ (σ.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
+lemma models_iff_provable_of_Delta1_param [V↓[ℒₒᵣ] ⊧* T] {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
+    V ⊧/(Nat.cast ∘ e) σ.val ↔ T ⊢ (σ.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
   calc
-    V ⊧/(e ·) σ.val ↔ ℕ ⊧/e σ.val        := by
+    V ⊧/(Nat.cast ∘ e) σ.val ↔ ℕ ⊧/e σ.val        := by
       simp [models_iff_of_Delta1 hσ hσV]
   _                 ↔ ℕ ⊧/e σ.sigma.val  := by
       simp [HierarchySymbol.Semiformula.val_sigma]