fx?

Author: SnO2WMaN

Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean

@@ -38,7 +38,7 @@ noncomputable abbrev toNumVec (w : Fin n → V) : SemitermVec V ℒₒᵣ n k :=
 
 variable (T)
 
-theorem term_complete {n : ℕ} (t : FirstOrder.ClosedArithmeticSemiterm n) (w : Fin n → V) :
+theorem term_complete {n : ℕ} (t : FirstOrder.ClosedSemiterm ℒₒᵣ n) (w : Fin n → V) :
     T.internalize V ⊢ (toNumVec w ⤕ ⌜t⌝) ≐  𝕹 (t.valbm V w) :=
   match t with
   |                         #z => by simp

Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Coding.lean

@@ -268,16 +268,16 @@ namespace Sentence
 def typed_quote_def (σ : Semisentence L n) :
     (⌜σ⌝ : Bootstrapping.Semiformula V L n) = ⌜(Rewriting.emb σ : SyntacticSemiformula L n)⌝ := rfl
 
-@[simp] lemma typed_quote_eq (t u : ClosedArithmeticSemiterm n) :
+@[simp] lemma typed_quote_eq (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t = !!u” : ArithmeticSemisentence n)⌝ : Bootstrapping.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≐ ⌜u⌝) := rfl
 
-@[simp] lemma typed_quote_ne (t u : ClosedArithmeticSemiterm n) :
+@[simp] lemma typed_quote_ne (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t ≠ !!u” : ArithmeticSemisentence n)⌝ : Bootstrapping.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≉ ⌜u⌝) := rfl
 
-@[simp] lemma typed_quote_lt (t u : ClosedArithmeticSemiterm n) :
+@[simp] lemma typed_quote_lt (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t < !!u” : ArithmeticSemisentence n)⌝ : Bootstrapping.Semiformula V ℒₒᵣ n) = (⌜t⌝ <' ⌜u⌝) := rfl
 
-@[simp] lemma typed_quote_nlt (t u : ClosedArithmeticSemiterm n) :
+@[simp] lemma typed_quote_nlt (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t ≮ !!u” : ArithmeticSemisentence n)⌝ : Bootstrapping.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≮' ⌜u⌝) := rfl
 
 noncomputable instance : GödelQuote (Semisentence L n) V where

Foundation/FirstOrder/Bootstrapping/Syntax/Term/Coding.lean

@@ -164,14 +164,14 @@ def empty_typed_quote_def (t : ClosedSemiterm L n) :
 @[simp] lemma empty_typed_quote_func (f : L.Func k) (v : Fin k → ClosedSemiterm L n) :
     (⌜func f v⌝ : Bootstrapping.Semiterm V L n) = Bootstrapping.Semiterm.func f fun i ↦ ⌜v i⌝ := rfl
 
-@[simp] lemma empty_typed_quote_add (t u : ClosedArithmeticSemiterm n) :
-    (⌜(‘!!t + !!u’ : ClosedArithmeticSemiterm n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = ⌜t⌝ + ⌜u⌝ := rfl
+@[simp] lemma empty_typed_quote_add (t u : ClosedSemiterm ℒₒᵣ n) :
+    (⌜(‘!!t + !!u’ : ClosedSemiterm ℒₒᵣ n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = ⌜t⌝ + ⌜u⌝ := rfl
 
-@[simp] lemma empty_typed_quote_mul (t u : ClosedArithmeticSemiterm n) :
-    (⌜(‘!!t * !!u’ : ClosedArithmeticSemiterm n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = ⌜t⌝ * ⌜u⌝ := rfl
+@[simp] lemma empty_typed_quote_mul (t u : ClosedSemiterm ℒₒᵣ n) :
+    (⌜(‘!!t * !!u’ : ClosedSemiterm ℒₒᵣ n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = ⌜t⌝ * ⌜u⌝ := rfl
 
 @[simp] lemma empty_typed_quote_numeral_eq_numeral (k : ℕ) :
-    (⌜(↑k : ClosedArithmeticSemiterm n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = typedNumeral ↑k := by
+    (⌜(↑k : ClosedSemiterm ℒₒᵣ n)⌝ : Bootstrapping.Semiterm V ℒₒᵣ n) = typedNumeral ↑k := by
   simp [empty_typed_quote_def]
 
 noncomputable instance : GödelQuote (ClosedSemiterm L n) V where