@@ -8,76 +8,78 @@ namespace LO.FirstOrder.Arithmetic
88open PeanoMinus R0
99
1010lemma nat_modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
11- ℕ ⊧/v φ ↔ ℕ ⊧ₘ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
12- simp [models_iff]
11+ φ.Evalb v ↔ ℕ↓[ℒₒᵣ] ⊧ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
12+ simp [models_iff, Function.comp_def, Matrix.empty_eq ]
1313
14- variable (V : Type *) [ORingStructure V] [V ⊧ₘ * 𝗣𝗔⁻]
14+ variable (V : Type *) [ORingStructure V] [V↓[ℒₒᵣ] ⊧ * 𝗣𝗔⁻]
1515
1616lemma modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
17- V ⊧/(v ·) φ ↔ V ⊧ₘ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
18- simp [models_iff, numeral_eq_natCast]
17+ φ.Evalb (M := V) (Nat.cast ∘ v) ↔ V↓[ℒₒᵣ] ⊧ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
18+ simp [models_iff, Function.comp_def, Matrix.empty_eq, numeral_eq_natCast]
1919
2020lemma shigmaZero_absolute {k} (φ : 𝚺₀.Semisentence k) (v : Fin k → ℕ) :
21- ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
21+ φ.val.Evalb v ↔ φ.val.Evalb (M := V) (Nat.cast ∘ v) :=
2222 ⟨by simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs] using nat_extention_sigmaOne V (by simp),
2323 by simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs] using nat_extention_piOne V (by simp)⟩
2424
2525lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop } {R' : (Fin k → V) → Prop } {φ : 𝚺₀.Semisentence k}
2626 (hR : 𝚺₀.Defined R φ) (hR' : 𝚺₀.Defined R' φ) (v : Fin k → ℕ) :
27- R v ↔ R' (fun i ↦ (v i : V) ) := by
27+ R v ↔ R' (Nat.cast ∘ v ) := by
2828 simpa [hR.iff, hR'.iff] using Arithmetic.shigmaZero_absolute V φ v
2929
3030lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1 )}
3131 (hf : 𝚺₀.DefinedFunction f φ) (hf' : 𝚺₀.DefinedFunction f' φ) (v : Fin k → ℕ) :
32- (f v : V) = f' (fun i ↦ (v i) ) := by
32+ (f v : V) = f' (Nat.cast ∘ v ) := by
3333 simpa using Defined.shigmaZero_absolute V hf hf' (f v :> v)
3434
3535lemma sigmaOne_upward_absolute {k} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
36- ℕ ⊧/v φ.val → V ⊧/(v ·) φ.val := by
36+ φ.val.Evalb v → φ.val.Evalb (M := V) (Nat.cast ∘ v) := by
3737 simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
3838 using nat_extention_sigmaOne V (by simp)
3939
4040lemma piOne_downward_absolute {k} (φ : 𝚷₁.Semisentence k) (v : Fin k → ℕ) :
41- V ⊧/(v ·) φ.val → ℕ ⊧/v φ.val := by
41+ φ.val.Evalb (M := V) (Nat.cast ∘ v) → φ.val.Evalb v := by
4242 simpa [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
4343 using nat_extention_piOne V (by simp)
4444
4545lemma deltaOne_absolute {k} (φ : 𝚫₁.Semisentence k)
4646 (properNat : φ.ProperOn ℕ) (proper : φ.ProperOn V) (v : Fin k → ℕ) :
47- ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
47+ φ.val.Evalb v ↔ φ.val.Evalb (M := V) (Nat.cast ∘ v) :=
4848 ⟨by simpa [HierarchySymbol.Semiformula.val_sigma] using sigmaOne_upward_absolute V φ.sigma v,
4949 by simpa [proper.iff', properNat.iff'] using piOne_downward_absolute V φ.pi v⟩
5050
5151lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop } {R' : (Fin k → V) → Prop } {φ : 𝚫₁.Semisentence k}
5252 (hR : 𝚫₁.Defined R φ) (hR' : 𝚫₁.Defined R' φ) (v : Fin k → ℕ) :
53- R v ↔ R' (fun i ↦ (v i : V) ) := by
53+ R v ↔ R' (Nat.cast ∘ v ) := by
5454 simpa using deltaOne_absolute V φ hR.proper hR'.proper v
5555
5656lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1 )}
5757 (hf : 𝚺₁.DefinedFunction f φ) (hf' : 𝚺₁.DefinedFunction f' φ) (v : Fin k → ℕ) :
58- (f v : V) = f' (fun i ↦ (v i) ) := by
58+ (f v : V) = f' (Nat.cast ∘ v ) := by
5959 simpa using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v)
6060
6161variable {V}
6262
6363lemma models_iff_of_Sigma0 {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
64- V ⊧/(e ·) σ ↔ ℕ ⊧/e σ := by
65- by_cases h : ℕ ⊧/e σ <;> simp [h]
66- · have : V ⊧/(e ·) σ := by
64+ σ.Evalb (M := V) (Nat.cast ∘ e) ↔ σ.Evalb e := by
65+ by_cases h : σ.Evalb e <;> simp [h]
66+ · have : σ.Evalb (M := V) (Nat.cast ∘ e) := by
6767 simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) h
6868 simpa [HierarchySymbol.Semiformula.val_sigma] using this
69- · have : ℕ ⊧/e (∼σ) := by simpa using h
70- have : V ⊧/(e ·) (∼σ) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) this
69+ · have : (∼σ).Evalb (M := ℕ) e := by simpa using h
70+ have : (∼σ).Evalb (M := V) (Nat.cast ∘ e) := by
71+ simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp [Hierarchy.of_zero hσ]) this
7172 simpa using this
7273
7374lemma models_iff_of_Delta1 {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
74- V ⊧/(e ·) σ.val ↔ ℕ ⊧/e σ.val := by
75- by_cases h : ℕ ⊧/e σ.val <;> simp [h]
76- · have : ℕ ⊧/e σ.sigma.val := by simpa [HierarchySymbol.Semiformula.val_sigma] using h
77- have : V ⊧/(e ·) σ.sigma.val := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
75+ σ.val.Evalb (M := V) (Nat.cast ∘ e) ↔ σ.val.Evalb e := by
76+ by_cases h : σ.val.Evalb e <;> simp [h]
77+ · have : σ.sigma.val.Evalb e := by simpa [HierarchySymbol.Semiformula.val_sigma] using h
78+ have : σ.sigma.val.Evalb (M := V) (Nat.cast ∘ e) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
7879 simpa [HierarchySymbol.Semiformula.val_sigma] using this
79- · have : ℕ ⊧/e (∼σ.pi.val) := by simpa [hσ.iff'] using h
80- have : V ⊧/(e ·) (∼σ.pi.val) := by simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
80+ · have : (∼σ.pi.val).Evalb (M := ℕ) e := by simpa [hσ.iff'] using h
81+ have : (∼σ.pi.val).Evalb (M := V) (Nat.cast ∘ e) := by
82+ simpa [numeral_eq_natCast] using bold_sigma_one_completeness' (M := V) (by simp) this
8183 simpa [hσV.iff'] using this
8284
8385variable {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] [T.SoundOnHierarchy 𝚺 1 ]
@@ -86,21 +88,21 @@ noncomputable instance : 𝗥₀ ⪯ T := Entailment.WeakerThan.trans (𝓣 :=
8688
8789theorem sigma_one_completeness_iff_param {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} :
8890 ℕ ⊧/e σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := Iff.trans
89- (by simp [models_iff, Semiformula.eval_substs])
91+ (by simp [models_iff, Semiformula.eval_substs, Function.comp_def, Matrix.empty_eq ])
9092 (sigma_one_completeness_iff (T := T) (by simp [hσ]))
9193
92- lemma models_iff_provable_of_Sigma0_param [V ⊧ₘ * T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
93- V ⊧/(e · ) σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
94+ lemma models_iff_provable_of_Sigma0_param [V↓[ℒₒᵣ] ⊧ * T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
95+ V ⊧/(Nat.cast ∘ e ) σ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
9496 calc
95- V ⊧/(e · ) σ ↔ ℕ ⊧/e σ := by
97+ V ⊧/(Nat.cast ∘ e ) σ ↔ ℕ ⊧/e σ := by
9698 simp [models_iff_of_Sigma0 hσ]
9799 _ ↔ T ⊢ (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
98100 apply sigma_one_completeness_iff_param (by simp [Hierarchy.of_zero hσ])
99101
100- lemma models_iff_provable_of_Delta1_param [V ⊧ₘ * T] {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
101- V ⊧/(e · ) σ.val ↔ T ⊢ (σ.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
102+ lemma models_iff_provable_of_Delta1_param [V↓[ℒₒᵣ] ⊧ * T] {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
103+ V ⊧/(Nat.cast ∘ e ) σ.val ↔ T ⊢ (σ.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
102104 calc
103- V ⊧/(e · ) σ.val ↔ ℕ ⊧/e σ.val := by
105+ V ⊧/(Nat.cast ∘ e ) σ.val ↔ ℕ ⊧/e σ.val := by
104106 simp [models_iff_of_Delta1 hσ hσV]
105107 _ ↔ ℕ ⊧/e σ.sigma.val := by
106108 simp [HierarchySymbol.Semiformula.val_sigma]
0 commit comments