instance definability

Arithmetization/Basic/IOpen.lean

@@ -184,7 +184,7 @@ lemma div_mul (a b c : M) : a / (b * c) = a / b / c := by
 
 instance div_polybounded : PolyBounded₂ ℒₒᵣ ((· / ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
 
-instance div_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν ((· / ·) : M → M → M) := defined_to_with_param₀ _ div_defined
+instance div_definable : DefinableFunction₂ ℒₒᵣ Σ 0 ((· / ·) : M → M → M) := defined_to_with_param _ div_defined
 
 @[simp] lemma div_mul_le (a b : M) : a / b * b ≤ a := by rw [mul_comm]; exact mul_div_le _ _
 
@@ -299,7 +299,7 @@ lemma rem_defined : Δ₀-Function₂ ((· % ·) : M → M → M) via remDef :=
   intro v; simp [Matrix.vecHead, Matrix.vecTail, remDef,
     rem_graph, Semiformula.eval_substs, div_defined.pval, sub_defined.pval, le_iff_lt_succ]
 
-instance rem_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν ((· % ·) : M → M → M) := defined_to_with_param₀ _ rem_defined
+instance rem_definable : DefinableFunction₂ ℒₒᵣ Σ 0 ((· % ·) : M → M → M) := defined_to_with_param _ rem_defined
 
 lemma div_add_mod (a b : M) : b * (a / b) + (a % b) = a :=
   add_tsub_self_of_le (mul_div_le a b)
@@ -459,7 +459,7 @@ def sqrtdef : Δ₀Sentence 2 :=
 lemma sqrt_defined : Δ₀-Function₁ (λ a : M ↦ √a) via sqrtdef := by
   intro v; simp[sqrt_graph, sqrtdef, Matrix.vecHead, Matrix.vecTail]
 
-instance sqrt_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν ((√·) : M → M) := defined_to_with_param₀ _ sqrt_defined
+instance sqrt_definable : DefinableFunction₁ ℒₒᵣ Σ 0 ((√·) : M → M) := defined_to_with_param₀ _ sqrt_defined
 
 lemma eq_sqrt (x a : M) : x * x ≤ a ∧ a < (x + 1) * (x + 1) → x = √a := Classical.choose_uniq (sqrt_exists_unique a)
 
@@ -550,7 +550,7 @@ def pairDef : Δ₀Sentence 3 := ⟨“(#1 < #2 ∧ #0 = #2 * #2 + #1) ∨ (#2 
 lemma pair_defined : Δ₀-Function₂ (λ a b : M ↦ ⟪a, b⟫) via pairDef := by
   intro v; simp [pair_graph, pairDef]
 
-instance pair_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (pair : M → M → M) := defined_to_with_param₀ _ pair_defined
+instance pair_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (pair : M → M → M) := defined_to_with_param₀ _ pair_defined
 
 instance : PolyBounded₂ ℒₒᵣ (pair : M → M → M) :=
   ⟨ᵀ“(#1 * #1 + #0) + (#0 * #0 + #0 + #1)”, by intro v; simp [pair]; split_ifs <;> try simp [pair, *]⟩
@@ -610,15 +610,15 @@ lemma pi₁_defined : Δ₀-Function₁ (pi₁ : M → M) via pi₁Def := by
   · intro h; exact ⟨π₂ v 1, by simp [←le_iff_lt_succ],  by simp [h]⟩
   · rintro ⟨a, _, e⟩; simp [e]
 
-instance pi₁_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (pi₁ : M → M) := defined_to_with_param₀ _ pi₁_defined
+instance pi₁_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (pi₁ : M → M) := defined_to_with_param₀ _ pi₁_defined
 
 lemma pi₂_defined : Δ₀-Function₁ (pi₂ : M → M) via pi₂Def := by
   intro v; simp [pi₂Def, pair_defined.pval]
   constructor
   · intro h; exact ⟨π₁ v 1, by simp [←le_iff_lt_succ], by simp [h]⟩
   · rintro ⟨a, _, e⟩; simp [e]
 
-instance pi₂_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (pi₂ : M → M) := defined_to_with_param₀ _ pi₂_defined
+instance pi₂_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (pi₂ : M → M) := defined_to_with_param₀ _ pi₂_defined
 
 end pair
 

Arithmetization/IDeltaZero/Exponential/Exp.lean

@@ -28,7 +28,7 @@ lemma ext_defined : Δ₀-Function₂ (λ a b : M ↦ ext a b) via extDef := by
   intro v; simp [Matrix.vecHead, Matrix.vecTail, extDef,
     ext_graph, Semiformula.eval_substs, div_defined.pval, rem_defined.pval, le_iff_lt_succ]
 
-instance ext_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (ext : M → M → M) := defined_to_with_param₀ _ ext_defined
+instance ext_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (ext : M → M → M) := defined_to_with_param _ ext_defined
 
 @[simp] lemma ext_le_add (u z : M) : ext u z ≤ z :=
   le_trans (mod_le (z / u) u) (by simp [add_comm])
@@ -112,7 +112,7 @@ def Exp.def : Δ₀Sentence 2 := ⟨
 lemma Exp.defined : Δ₀-Relation (Exp : M → M → Prop) via Exp.def := by
   intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval, Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq]
 
-instance exp_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν (Exp : M → M → Prop) := defined_to_with_param₀ _ Exp.defined
+instance exp_definable : DefinableRel ℒₒᵣ Σ 0 (Exp : M → M → Prop) := defined_to_with_param _ Exp.defined
 
 namespace Exp
 
@@ -717,7 +717,7 @@ def expdef : Δ₀Sentence 2 := ⟨“!Exp.def [#1, #0]”, by simp⟩
 lemma exp_defined : Δ₀-Function₁ (exponential : M → M) via expdef := by
   intro v; simp [expdef, exponential_graph, Exp.defined.pval]
 
-instance exponential_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (exponential : M → M) := defined_to_with_param₀ _ exp_defined
+instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (exponential : M → M) := defined_to_with_param _ exp_defined
 
 lemma exponential_of_exp {a b : M} (h : Exp a b) : exp a = b :=
   Eq.symm <| exponential_graph.mpr h

Arithmetization/IDeltaZero/Exponential/Log.lean

@@ -72,7 +72,7 @@ def logDef : Δ₀Sentence 2 := ⟨“(#1 = 0 → #0 = 0) ∧ (0 < #1 → #0 < #
 lemma log_defined : Δ₀-Function₁ (log : M → M) via logDef := by
   intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ]
 
-instance log_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (log : M → M) := defined_to_with_param₀ _ log_defined
+instance log_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (log : M → M) := defined_to_with_param _ log_defined
 
 instance : PolyBounded₁ ℒₒᵣ (log : M → M) := ⟨#0, λ _ ↦ by simp⟩
 
@@ -163,7 +163,7 @@ def lengthDef : Δ₀Sentence 2 := ⟨“(0 < #1 → ∃[#0 < #2 + 1] (!logDef [
 lemma length_defined : Δ₀-Function₁ (‖·‖ : M → M) via lengthDef := by
   intro v; simp [lengthDef, length_graph, log_defined.pval, ←le_iff_lt_succ]
 
-instance length_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (‖·‖ : M → M) := defined_to_with_param₀ _ length_defined
+instance length_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (‖·‖ : M → M) := defined_to_with_param _ length_defined
 
 instance : PolyBounded₁ ℒₒᵣ (‖·‖ : M → M) := ⟨#0, λ _ ↦ by simp⟩
 
@@ -334,7 +334,7 @@ def bexpDef : Δ₀Sentence 3 := ⟨“∃[#0 < #2 + 1] (!lengthDef [#0, #2] ∧
 lemma bexp_defined : Δ₀-Function₂ (bexp : M → M → M) via bexpDef := by
   intro v; simp [bexpDef, bexp_graph, Exp.defined.pval, length_defined.pval, ←le_iff_lt_succ]
 
-instance bexp_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (bexp : M → M → M) := defined_to_with_param₀ _ bexp_defined
+instance bexp_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (bexp : M → M → M) := defined_to_with_param _ bexp_defined
 
 instance : PolyBounded₂ ℒₒᵣ (bexp : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
 
@@ -413,7 +413,7 @@ lemma fbit_defined : Δ₀-Function₂ (fbit : M → M → M) via fbitDef := by
   · intro h; exact ⟨bexp (v 1) (v 2), by simp, rfl, _, by simp, rfl, h⟩
   · rintro ⟨_, _, rfl, _, _, rfl, h⟩; exact h
 
-instance fbit_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (fbit : M → M → M) := defined_to_with_param₀ _ fbit_defined
+instance fbit_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (fbit : M → M → M) := defined_to_with_param _ fbit_defined
 
 instance : PolyBounded₂ ℒₒᵣ (fbit : M → M → M) := ⟨ᵀ“1”, λ _ ↦ by simp⟩
 

Arithmetization/IDeltaZero/Exponential/PPow2.lean

@@ -38,7 +38,7 @@ def ppow2Def : Δ₀Sentence 1 :=
 lemma ppow2_defined : Δ₀-Predicate (PPow2 : M → Prop) via ppow2Def := by
   intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval]
 
-instance ppow2_definable (Γ ν) : DefinablePred ℒₒᵣ Γ ν (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined
+instance ppow2_definable : DefinablePred ℒₒᵣ Σ 0 (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined
 
 namespace SPPow2
 

Arithmetization/IDeltaZero/Exponential/Pow2.lean

@@ -24,7 +24,7 @@ lemma pow2_defined : Δ₀-Predicate (Pow2 : M → Prop) via pow2Def := by
   simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
     Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval]
 
-instance pow2_definable (Γ ν) : DefinablePred ℒₒᵣ Γ ν (Pow2 : M → Prop) := defined_to_with_param₀ _ pow2_defined
+instance pow2_definable : DefinablePred ℒₒᵣ Σ 0 (Pow2 : M → Prop) := defined_to_with_param _ pow2_defined
 
 lemma Pow2.pos {a : M} (h : Pow2 a) : 0 < a := h.1
 
@@ -119,7 +119,7 @@ lemma lenbit_defined : Δ₀-Relation (LenBit : M → M → Prop) via lenbitDef
   · intro h; exact ⟨v 1 / v 0, by simp, rfl, h⟩
   · rintro ⟨z, hz, rfl, h⟩; exact h
 
-instance lenbit_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν (LenBit : M → M → Prop) := defined_to_with_param₀ _ lenbit_defined
+instance lenbit_definable : DefinableRel ℒₒᵣ Σ 0 (LenBit : M → M → Prop) := defined_to_with_param _ lenbit_defined
 
 lemma LenBit.le {i a : M} (h : LenBit i a) : i ≤ a := by
   by_contra A; simp [LenBit, show a < i from by simpa using A] at h

Arithmetization/ISigmaOne/Bit.lean

@@ -27,7 +27,7 @@ lemma bit_defined : Δ₀-Relation ((· ∈ ·) : M → M → Prop) via bitDef :
   · intro h; exact ⟨exp (v 0), by simp [h.le], rfl, h⟩
   · rintro ⟨_, _, rfl, h⟩; exact h
 
-instance mem_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν ((· ∈ ·) : M → M → Prop) := defined_to_with_param₀ _ bit_defined
+instance mem_definable : DefinableRel ℒₒᵣ Σ 0 ((· ∈ ·) : M → M → Prop) := defined_to_with_param _ bit_defined
 
 open Classical in
 noncomputable def bitInsert (i a : M) : M := if i ∈ a then a else a + exp i
@@ -137,7 +137,7 @@ lemma bitSubset_defined : Δ₀-Relation ((· ⊆ ·) : M → M → Prop) via bi
   intro v; simp [bitSubsetDef, bit_defined.pval]
   exact ⟨by intro h x _ hx; exact h hx, by intro h x hx; exact h x (lt_of_mem hx) hx⟩
 
-instance bitSubset_definable (Γ ν) : DefinableRel ℒₒᵣ Γ ν ((· ⊆ ·) : M → M → Prop) := defined_to_with_param₀ _ bitSubset_defined
+instance bitSubset_definable : DefinableRel ℒₒᵣ Σ 0 ((· ⊆ ·) : M → M → Prop) := defined_to_with_param₀ _ bitSubset_defined
 
 lemma mem_exp_add_succ_sub_one (i j : M) : i ∈ exp (i + j + 1) - 1 := by
   have : exp (i + j + 1) - 1 = (exp j - 1) * exp (i + 1) + exp i + (exp i - 1) := calc
@@ -215,7 +215,7 @@ theorem finset_comprehension {P : M → Prop} (hP : Γ(ν)-Predicate P) (n : M)
   have : (Γ.alt)(ν)-Predicate (fun s ↦ ∀ i < n, P i → i ∈ s) := by
     apply Definable.ball_lt; simp; apply Definable.imp
     definability
-    simp [mem_definable]
+    apply @Definable.of_sigma_zero M ℒₒᵣ _ _ _ _ mem_definable
   have : ∃ t, (∀ i < n, P i → i ∈ t) ∧ ∀ t' < t, ∃ x, P x ∧ x < n ∧ x ∉ t' := by
     simpa using least_number_h (L := ℒₒᵣ) Γ.alt ν this hs
   rcases this with ⟨t, ht, t_minimal⟩

Arithmetization/OmegaOne/Basic.lean

@@ -67,7 +67,7 @@ lemma hash_defined : Δ₀-Function₂ (Hash.hash : M → M → M) via hashDef :
   · intro h; exact ⟨‖v 1‖, by simp, ‖v 2‖, by simp, rfl, rfl, by rw [h]; exact exp_hash _ _⟩
   · rintro ⟨_, _, _, _, rfl, rfl, h⟩; exact h.uniq (exp_hash (v 1) (v 2))
 
-instance hash_definable (Γ ν) : DefinableFunction₂ ℒₒᵣ Γ ν (Hash.hash : M → M → M) := defined_to_with_param₀ _ hash_defined
+instance hash_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (Hash.hash : M → M → M) := defined_to_with_param _ hash_defined
 
 @[simp] lemma hash_pow2 (a b : M) : Pow2 (a # b) := (exp_hash a b).range_pow2
 

Arithmetization/OmegaOne/Nuon.lean

@@ -82,7 +82,7 @@ def extDef : Δ₀Sentence 4 :=
 lemma ext_defined : Δ₀-Function₃ (ext : M → M → M → M) via extDef := by
   intro v; simp [extDef, length_defined.pval, Exp.defined.pval, div_defined.pval, rem_defined.pval, lt_succ_iff_le, ext_graph]
 
-instance ext_Definable (Γ ν) : DefinableFunction₃ ℒₒᵣ Γ ν (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined
+instance ext_Definable : DefinableFunction₃ ℒₒᵣ Σ 0 (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined
 
 instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
 
@@ -565,7 +565,7 @@ lemma nuonAux_defined : Δ₀-Relation₃ (NuonAux : M → M → M → Prop) via
     length_defined.pval, sqrt_defined.pval, bexp_defined.pval, seriesSegmentDef_defined.pval, lt_succ_iff_le]
   rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]; simp
 
-instance nuonAux_definable (Γ ν) : DefinableRel₃ ℒₒᵣ Γ ν (NuonAux : M → M → M → Prop) := defined_to_with_param₀ _ nuonAux_defined
+instance nuonAux_definable : DefinableRel₃ ℒₒᵣ Σ 0 (NuonAux : M → M → M → Prop) := defined_to_with_param _ nuonAux_defined
 
 instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
 
@@ -679,7 +679,7 @@ lemma nuon_defined : Δ₀-Function₁ (nuon : M → M) via nuonDef := by
     length_defined.pval, Nuon.nuonAux_defined.pval, lt_succ_iff_le]
   rw [Nuon.bex_eq_le_iff]; simp
 
-instance nuon_definable (Γ ν) : DefinableFunction₁ ℒₒᵣ Γ ν (nuon : M → M) := defined_to_with_param₀ _ nuon_defined
+instance nuon_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (nuon : M → M) := defined_to_with_param _ nuon_defined
 
 end Model