Merge pull request #3 from FormalizedFormalLogic/redefine_term_formula

Redefine term & formula

Arithmetization/Basic/IOpen.lean

@@ -846,6 +846,8 @@ lemma nat_cast_pair (n m : ℕ) : (⟪n, m⟫ : ℕ) = ⟪(n : V), (m : V)⟫ :=
 
 lemma nat_pair_eq (m n : ℕ) : ⟪n, m⟫ = Nat.pair n m := by simp [Arith.pair, Nat.pair]; congr
 
+lemma pair_coe_eq_coe_pair (m n : ℕ) :  ⟪n, m⟫ = (Nat.pair n m : V) := by simp [nat_cast_pair, nat_pair_eq]
+
 end
 
 end LO.Arith

Arithmetization/Definability/Boldface.lean

@@ -66,6 +66,9 @@ abbrev DefinedFunction {k} (f : (Fin k → V) → V) (p : ℌ.Semisentence (k +
 
 variable (ℌ)
 
+abbrev DefinedFunction₀ (c : V) (p : ℌ.Semisentence 1) : Prop :=
+  DefinedFunction (fun _ => c) p
+
 abbrev DefinedFunction₁ (f : V → V) (p : ℌ.Semisentence 2) : Prop :=
   DefinedFunction (fun v => f (v 0)) p
 
@@ -95,6 +98,8 @@ abbrev BoldfaceRel₆ (P : V → V → V → V → V → V → Prop) : Prop := 
 
 abbrev BoldfaceFunction (f : (Fin k → V) → V) : Prop := ℌ.Boldface (k := k + 1) (fun v ↦ v 0 = f (v ·.succ))
 
+abbrev BoldfaceFunction₀ (c : V) : Prop := ℌ.BoldfaceFunction (k := 0) (fun _ ↦ c)
+
 abbrev BoldfaceFunction₁ (f : V → V) : Prop := ℌ.BoldfaceFunction (k := 1) (fun v ↦ f (v 0))
 
 abbrev BoldfaceFunction₂ (f : V → V → V) : Prop := ℌ.BoldfaceFunction (k := 2) (fun v ↦ f (v 0) (v 1))
@@ -115,6 +120,8 @@ notation Γ "-Relation₃ " P " via " p => DefinedRel₃ Γ P p
 
 notation Γ "-Relation₄ " P " via " p => DefinedRel₄ Γ P p
 
+notation Γ "-Function₀ " c " via " p => DefinedFunction₀ Γ c p
+
 notation Γ "-Function₁ " f " via " p => DefinedFunction₁ Γ f p
 
 notation Γ "-Function₂ " f " via " p => DefinedFunction₂ Γ f p
@@ -389,7 +396,7 @@ lemma of_sigma_of_pi (hσ : 𝚺-[m].Boldface P) (hπ : 𝚷-[m].Boldface P) : 
 lemma of_zero (h : Γ'-[0].Boldface P) : ℌ.Boldface P := by
   rcases h with ⟨⟨p, hp⟩⟩; exact hp.to_definable₀
 
-lemma of_deltaOne (h : 𝚫₁.Boldface P) (Γ m) : Γ-[m + 1].Boldface P := by
+lemma of_deltaOne (h : 𝚫₁.Boldface P) {Γ m} : Γ-[m + 1].Boldface P := by
   rcases h with ⟨⟨p, hp⟩⟩; exact hp.to_definable_deltaOne
 
 instance [𝚺₀.Boldface P] (ℌ : HierarchySymbol) : ℌ.Boldface P := Boldface.of_zero (Γ' := 𝚺) (ℌ := ℌ) inferInstance
@@ -683,7 +690,7 @@ instance {k} {f : (Fin k → V) → V} [h : 𝚺-[m].BoldfaceFunction f] : 𝚫-
 instance {k} {f : (Fin k → V) → V} [𝚺₀.BoldfaceFunction f] : ℌ.BoldfaceFunction f := inferInstance
 
 lemma of_sigmaOne {k} {f : (Fin k → V) → V}
-    (h : 𝚺₁.BoldfaceFunction f) (Γ m) : Γ-[m + 1].BoldfaceFunction f := Boldface.of_deltaOne (graph_delta h) Γ m
+    (h : 𝚺₁.BoldfaceFunction f) {Γ m} : Γ-[m + 1].BoldfaceFunction f := Boldface.of_deltaOne (graph_delta h)
 
 @[simp] lemma var {k} (i : Fin k) : ℌ.BoldfaceFunction (fun v : Fin k → V ↦ v i) :=
   .of_zero (Γ' := 𝚺) ⟨.mkSigma “x | x = !!#i.succ” (by simp), by intro _; simp⟩

Arithmetization/ISigmaOne/HFS/Fixpoint.lean

@@ -128,9 +128,7 @@ lemma termSet_defined : 𝚺₁.DefinedFunction (fun v ↦ c.limSeq (v ·.succ)
 instance limSeq_definable :
   𝚺₁.BoldfaceFunction (fun v ↦ c.limSeq (v ·.succ) (v 0)) := c.termSet_defined.to_definable
 
-@[simp, definability] instance limSeq_definable' (Γ) :
-    Γ-[m + 1].BoldfaceFunction (fun v ↦ c.limSeq (v ·.succ) (v 0))  :=
-  .of_sigmaOne c.limSeq_definable _ _
+@[simp, definability] instance limSeq_definable' (Γ) : Γ-[m + 1].BoldfaceFunction (fun v ↦ c.limSeq (v ·.succ) (v 0)) := c.limSeq_definable.of_sigmaOne
 
 lemma mem_limSeq_succ_iff {x s : V} :
     x ∈ c.limSeq v (s + 1) ↔ x ≤ s ∧ c.Φ v {z | z ∈ c.limSeq v s} x := by simp [limSeq_succ, mem_succ_iff]

Arithmetization/ISigmaOne/HFS/Seq.lean

@@ -376,7 +376,7 @@ lemma mkSeq₂_defined : 𝚺₁-Function₂ (fun x y : V ↦ !⟦x, y⟧) via m
 
 instance mkSeq₂_definable : 𝚺₁-Function₂ (fun x y : V ↦ !⟦x, y⟧) := mkSeq₂_defined.to_definable
 
-instance mkSeq₂_definable' (Γ m) : Γ-[m + 1]-Function₂ (fun x y : V ↦ !⟦x, y⟧) := .of_sigmaOne mkSeq₂_definable _ _
+instance mkSeq₂_definable' (Γ m) : Γ-[m + 1]-Function₂ (fun x y : V ↦ !⟦x, y⟧) := mkSeq₂_definable.of_sigmaOne
 
 end
 
@@ -423,7 +423,7 @@ lemma mem_vectoSeq {n : ℕ} (v : Fin n → V) (i : Fin n) : ⟪(i : V), v i⟫
 
 end seqToVec
 
-lemma sigma₁_order_ball_induction {f : V → V → V} (hf : 𝚺₁-Function₂ f) {P : V → V → Prop} (hP : 𝚺₁-Relation P)
+lemma order_ball_induction_sigma1 {f : V → V → V} (hf : 𝚺₁-Function₂ f) {P : V → V → Prop} (hP : 𝚺₁-Relation P)
     (ind : ∀ x y, (∀ x' < x, ∀ y' ≤ f x y, P x' y') → P x y) : ∀ x y, P x y := by
   have maxf : ∀ x y, ∃ m, ∀ x' ≤ x, ∀ y' ≤ y, f x' y' ≤ m := by
     intro x y;
@@ -517,6 +517,73 @@ lemma sigma₁_order_ball_induction {f : V → V → V} (hf : 𝚺₁-Function
       exact ih m₁ (by simp [m₁]) (by simp [m₁]) x'' (lt_succ_iff_le.mp (lt_of_lt_of_le hx'' hx')) y'' (le_trans hy'' this)
   exact this x (by rfl) y (lt_of_mem_rng hW₀) (by simpa using hW₀) x (by rfl) y (by rfl)
 
+lemma order_ball_induction_sigma1' {f : V → V} (hf : 𝚺₁-Function₁ f) {P : V → V → Prop} (hP : 𝚺₁-Relation P)
+    (ind : ∀ x y, (∀ x' < x, ∀ y' ≤ f y, P x' y') → P x y) : ∀ x y, P x y :=
+  have : 𝚺₁-Function₂ (fun _ ↦ f) := FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₁ (by simp)
+  order_ball_induction_sigma1 this hP ind
+
+lemma order_ball_induction₂_sigma1 {fy fz : V → V → V → V}
+    (hfy : 𝚺₁-Function₃ fy) (hfz : 𝚺₁-Function₃ fz) {P : V → V → V → Prop} (hP : 𝚺₁-Relation₃ P)
+    (ind : ∀ x y z, (∀ x' < x, ∀ y' ≤ fy x y z, ∀ z' ≤ fz x y z, P x' y' z') → P x y z) : ∀ x y z, P x y z := by
+  let Q : V → V → Prop := fun x w ↦ P x (π₁ w) (π₂ w)
+  have hQ : 𝚺₁-Relation Q := by
+    simp [Q]
+    apply HierarchySymbol.Boldface.comp₃ (HierarchySymbol.BoldfaceFunction.var _)
+      (HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _))
+      (HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _))
+  let f : V → V → V := fun x w ↦ ⟪fy x (π₁ w) (π₂ w), fz x (π₁ w) (π₂ w)⟫
+  have hf : 𝚺₁-Function₂ f := by
+    simp [f]
+    apply HierarchySymbol.BoldfaceFunction.comp₂
+    · apply HierarchySymbol.BoldfaceFunction.comp₃ (HierarchySymbol.BoldfaceFunction.var _)
+      · apply HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _)
+      · apply HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _)
+    · apply HierarchySymbol.BoldfaceFunction.comp₃ (HierarchySymbol.BoldfaceFunction.var _)
+      · apply HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _)
+      · apply HierarchySymbol.BoldfaceFunction.comp₁ (HierarchySymbol.BoldfaceFunction.var _)
+  intro x y z
+  simpa [Q] using order_ball_induction_sigma1 hf hQ (fun x w ih ↦
+    ind x (π₁ w) (π₂ w) (fun x' hx' y' hy' z' hz' ↦ by simpa [Q] using ih x' hx' ⟪y', z'⟫ (pair_le_pair hy' hz')))
+    x ⟪y, z⟫
+
+lemma order_ball_induction₃_sigma1 {fy fz fw : V → V → V → V → V}
+    (hfy : 𝚺₁-Function₄ fy) (hfz : 𝚺₁-Function₄ fz) (hfw : 𝚺₁-Function₄ fw) {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P)
+    (ind : ∀ x y z w, (∀ x' < x, ∀ y' ≤ fy x y z w, ∀ z' ≤ fz x y z w, ∀ w' ≤ fw x y z w, P x' y' z' w') → P x y z w) : ∀ x y z w, P x y z w := by
+  let Q : V → V → Prop := fun x v ↦ P x (π₁ v) (π₁ (π₂ v)) (π₂ (π₂ v))
+  have hQ : 𝚺₁-Relation Q := by
+    simp [Q]
+    apply HierarchySymbol.Boldface.comp₄
+      (HierarchySymbol.BoldfaceFunction.var _)
+      (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+      (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+      (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+  let f : V → V → V := fun x v ↦ ⟪fy x (π₁ v) (π₁ (π₂ v)) (π₂ (π₂ v)), fz x (π₁ v) (π₁ (π₂ v)) (π₂ (π₂ v)), fw x (π₁ v) (π₁ (π₂ v)) (π₂ (π₂ v))⟫
+  have hf : 𝚺₁-Function₂ f := by
+    simp [f]
+    apply HierarchySymbol.BoldfaceFunction.comp₂
+    · apply HierarchySymbol.BoldfaceFunction.comp₄
+        (HierarchySymbol.BoldfaceFunction.var _)
+        (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+        (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+        (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+    · apply HierarchySymbol.BoldfaceFunction.comp₂
+      · apply HierarchySymbol.BoldfaceFunction.comp₄
+          (HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+      · apply HierarchySymbol.BoldfaceFunction.comp₄
+          (HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+          (HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.comp₁ <| HierarchySymbol.BoldfaceFunction.var _)
+  intro x y z w
+  have := order_ball_induction_sigma1 hf hQ (fun x v ih ↦
+    ind x (π₁ v) (π₁ (π₂ v)) (π₂ (π₂ v)) (fun x' hx' y' hy' z' hz' w' hw' ↦ by
+      simpa [Q] using ih x' hx' ⟪y', z', w'⟫ (pair_le_pair hy' <| pair_le_pair hz' hw')))
+    x ⟪y, z, w⟫
+  simpa [Q] using this
+
 end LO.Arith
 
 end

Arithmetization/ISigmaOne/HFS/Supplemental.lean

@@ -109,8 +109,7 @@ lemma seqExp_defined : 𝚺₁-Function₂ (seqExp : V → V → V) via seqExpDe
 
 instance seqExp_definable : 𝚺₁-Function₂ (seqExp : V → V → V) := seqExp_defined.to_definable
 
-@[simp, definability] instance seqExp_definable' (Γ) : Γ-[m + 1]-Function₂ (seqExp : V → V → V) :=
-  .of_sigmaOne seqExp_definable _ _
+instance seqExp_definable' (Γ) : Γ-[m + 1]-Function₂ (seqExp : V → V → V) := seqExp_definable.of_sigmaOne
 
 lemma mem_seqExp_iff {s a k : V} : s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ (∀ i z, ⟪i, z⟫ ∈ s → z ∈ a) := by
   induction k using induction_pi1 generalizing s