Update (v4.16)

Incompleteness/Arith/D3.lean

@@ -63,7 +63,7 @@ def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).SemitermVec n
 
 namespace TProof
 
-open Language.Theory.TProof System
+open Language.Theory.TProof Entailment
 
 variable (T)
 

Incompleteness/Arith/DC.lean

@@ -10,9 +10,9 @@ namespace LO.FirstOrder.Arith
 
 open LO.Arith LO.Arith.Formalized
 
-variable (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T]
+variable (T : Theory ℒₒᵣ) [𝐈𝚺₁ ⪯ T]
 
-variable (U : Theory ℒₒᵣ) [U.Delta1Definable] [ℕ ⊧ₘ* U] [𝐑₀ ≼ U]
+variable (U : Theory ℒₒᵣ) [U.Delta1Definable] [ℕ ⊧ₘ* U] [𝐑₀ ⪯ U]
 
 instance : Diagonalization T where
   fixpoint := fixpoint

Incompleteness/Arith/First.lean

@@ -16,7 +16,7 @@ namespace LO.FirstOrder
 
 namespace Arith
 
-open LO.Arith LO.System LO.Arith.Formalized
+open LO.Arith LO.Entailment LO.Arith.Formalized
 
 lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by
   constructor
@@ -28,10 +28,10 @@ lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by
       (f := fun x : ℕ ↦ x ::ᵥ List.Vector.nil) (Primrec.to_comp <| Primrec.vector_cons.comp .id (.const _))
     exact this.of_eq <| by intro x; symm; simpa [List.Vector.cons_get] using hφ ![x];
 
-variable (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable]
+variable (T : Theory ℒₒᵣ) [𝐑₀ ⪯ T] [Sigma1Sound T] [T.Delta1Definable]
 
 /-- Gödel's First Incompleteness Theorem-/
-theorem goedel_first_incompleteness : ¬System.Complete T := by
+theorem goedel_first_incompleteness : ¬Entailment.Complete T := by
   let D : ℕ → Prop := fun n : ℕ ↦ ∃ φ : SyntacticSemiformula ℒₒᵣ 1, n = ⌜φ⌝ ∧ T ⊢! ∼φ/[⌜φ⌝]
   have D_re : RePred D := by
     have : 𝚺₁-Predicate fun φ : ℕ ↦
@@ -49,13 +49,13 @@ theorem goedel_first_incompleteness : ¬System.Complete T := by
     simpa [Semiformula.coe_substs_eq_substs_coe₁] using re_complete (T := T) (D_re) (x := n)
   have : T ⊢! ∼ρ ↔ T ⊢! ρ := by
     simpa [D, goedelNumber'_def, quote_eq_encode] using this ⌜σ⌝
-  have con : System.Consistent T := consistent_of_sigma1Sound T
-  refine LO.System.incomplete_iff_exists_undecidable.mpr ⟨↑ρ, ?_, ?_⟩
+  have con : Entailment.Consistent T := consistent_of_sigma1Sound T
+  refine LO.Entailment.incomplete_iff_exists_undecidable.mpr ⟨↑ρ, ?_, ?_⟩
   · intro h
     have : T ⊢! ∼↑ρ := by simpa [provable₀_iff] using this.mpr h
-    exact LO.System.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable h this) inferInstance
+    exact LO.Entailment.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable h this) inferInstance
   · intro h
     have : T ⊢! ↑ρ := this.mp (by simpa [provable₀_iff] using h)
-    exact LO.System.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h) inferInstance
+    exact LO.Entailment.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h) inferInstance
 
 end LO.FirstOrder.Arith

Incompleteness/Arith/FormalizedArithmetic.lean

@@ -58,7 +58,7 @@ variable (T : LOR.TTheory (V := V))
 
 namespace TProof
 
-open Language.Theory.TProof System System.FiniteContext
+open Language.Theory.TProof Entailment Entailment.FiniteContext
 
 section R₀Theory
 
@@ -295,7 +295,7 @@ noncomputable def bexIntro (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i
     T ⊢ φ.bex ↑n := by
   apply ex i
   suffices T ⊢ i <' n ⋏ φ^/[(i : ⌜ℒₒᵣ⌝.Term).sing] by simpa
-  exact System.andIntro (ltComplete T hi) b
+  exact Entailment.andIntro (ltComplete T hi) b
 
 lemma bex_intro! (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i}
     (hi : i < n) (b : T ⊢! φ ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) :

Incompleteness/Arith/Second.lean

@@ -83,7 +83,7 @@ namespace LO.FirstOrder.Arith
 
 open LO.Arith LO.Arith.Formalized
 
-variable {T : Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T]
+variable {T : Theory ℒₒᵣ} [𝐈𝚺₁ ⪯ T]
 
 section Diagonalization
 
@@ -101,9 +101,9 @@ lemma fixpoint_eq (θ : Semisentence ℒₒᵣ 1) :
 
 theorem diagonal (θ : Semisentence ℒₒᵣ 1) :
     T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝] :=
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
-    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance
     simp [models_iff]
     let Θ : V → Prop := fun x ↦ Semiformula.Evalbm V ![x] θ
     calc
@@ -125,9 +125,9 @@ def multifixpoint (θ : Fin k → Semisentence ℒₒᵣ k) (i : Fin k) : Senten
 
 theorem multidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) :
     T ⊢!. multifixpoint θ i ⭤ (Rew.substs fun j ↦ ⌜multifixpoint θ j⌝) ▹ (θ i) :=
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
-    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance
     suffices V ⊧/![] (multifixpoint θ i) ↔ V ⊧/(fun i ↦ ⌜multifixpoint θ i⌝) (θ i) by simpa [models_iff]
     let t : Fin k → V := fun i ↦ ⌜multidiag (θ i)⌝
     have ht : ∀ i, substNumerals (t i) t = ⌜multifixpoint θ i⌝ := by
@@ -157,24 +157,24 @@ variable {U : Theory ℒₒᵣ} [U.Delta1Definable]
 
 theorem provableₐ_D1 {σ} : U ⊢!. σ → T ⊢!. U.bewₐ σ := by
   intro h
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   apply complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
-    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance
     simpa [models_iff] using provableₐ_of_provable (T := U) (V := V) h
 
 theorem provableₐ_D2 {σ π} : T ⊢!. U.bewₐ (σ ➝ π) ➝ U.bewₐ σ ➝ U.bewₐ π :=
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
-    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance
     simp [models_iff]
     intro hσπ hσ
     exact provableₐ_iff.mpr <| (by simpa using provableₐ_iff.mp hσπ) ⨀ provableₐ_iff.mp hσ
 
 lemma provableₐ_sigma₁_complete {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) :
     T ⊢!. σ ➝ U.bewₐ σ :=
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
-    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance
     simpa [models_iff] using sigma₁_complete (T := U) (V := V) hσ
 
 theorem provableₐ_D3 {σ : Sentence ℒₒᵣ} :
@@ -183,16 +183,16 @@ theorem provableₐ_D3 {σ : Sentence ℒₒᵣ} :
 lemma goedel_iff_unprovable_goedel : T ⊢!. U.goedelₐ ⭤ ∼U.bewₐ U.goedelₐ := by
   simpa [Theory.goedelₐ, Theory.bewₐ] using diagonal (∼U.provableₐ)
 
-open LO.System LO.System.FiniteContext
+open LO.Entailment LO.Entailment.FiniteContext
 
 lemma provableₐ_D2_context {Γ σ π} (hσπ : Γ ⊢[T.alt]! (U.bewₐ (σ ➝ π))) (hσ : Γ ⊢[T.alt]! U.bewₐ σ) :
     Γ ⊢[T.alt]! U.bewₐ π := of'! provableₐ_D2 ⨀ hσπ ⨀ hσ
 
 lemma provableₐ_D3_context {Γ σ} (hσπ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ (U.bewₐ σ) := of'! provableₐ_D3 ⨀ hσπ
 
-variable [ℕ ⊧ₘ* T] [𝐑₀ ≼ U]
+variable [ℕ ⊧ₘ* T] [𝐑₀ ⪯ U]
 
-omit [𝐈𝚺₁ ≼ T] in
+omit [𝐈𝚺₁ ⪯ T] in
 lemma provableₐ_sound {σ} : T ⊢!. U.bewₐ σ → U ⊢! ↑σ := by
   intro h
   have : U.Provableₐ (⌜σ⌝ : ℕ) := by simpa [models₀_iff] using consequence_iff.mp (sound! (T := T) h) ℕ inferInstance
@@ -209,23 +209,23 @@ variable (T)
 
 variable [T.Delta1Definable]
 
-open LO.System LO.System.FiniteContext
+open LO.Entailment LO.Entailment.FiniteContext
 
 local notation "𝗚" => T.goedelₐ
 
 local notation "𝗖𝗼𝗻" => T.consistentₐ
 
 local prefix:max "□" => T.bewₐ
 
-lemma goedel_unprovable [System.Consistent T] : T ⊬ ↑𝗚 := by
+lemma goedel_unprovable [Entailment.Consistent T] : T ⊬ ↑𝗚 := by
   intro h
   have hp : T ⊢! ↑□𝗚 := provableₐ_D1 h
   have hn : T ⊢! ∼↑□𝗚 := by simpa [provable₀_iff] using and_left! goedel_iff_unprovable_goedel ⨀ h
   exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable hp hn) inferInstance
 
 lemma not_goedel_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗚 := fun h ↦ by
-  haveI : 𝐑₀ ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
-  have : T ⊢!. □𝗚 := System.contra₂'! (and_right! goedel_iff_unprovable_goedel) ⨀ (by simpa [provable₀_iff] using h)
+  haveI : 𝐑₀ ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  have : T ⊢!. □𝗚 := Entailment.contra₂'! (and_right! goedel_iff_unprovable_goedel) ⨀ (by simpa [provable₀_iff] using h)
   have : T ⊢! ↑𝗚 := provableₐ_sound this
   exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h)
     (Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩)
@@ -248,13 +248,13 @@ lemma consistent_iff_goedel : T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚 := by
     simpa [provable₀_iff] using  contra₁'! (deduct'! this)
 
 /-- Gödel's Second Incompleteness Theorem-/
-theorem goedel_second_incompleteness [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦
+theorem goedel_second_incompleteness [Entailment.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦
   goedel_unprovable T <| and_left! (consistent_iff_goedel T) ⨀ h
 
 theorem inconsistent_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗖𝗼𝗻 := fun h ↦
   not_goedel_unprovable T <| contra₀'! (and_right! (consistent_iff_goedel T)) ⨀ h
 
-theorem inconsistent_undecidable [ℕ ⊧ₘ* T] : System.Undecidable T ↑𝗖𝗼𝗻 := by
+theorem inconsistent_undecidable [ℕ ⊧ₘ* T] : Entailment.Undecidable T ↑𝗖𝗼𝗻 := by
   haveI : Consistent T := Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩
   constructor
   · exact goedel_second_incompleteness T

Incompleteness/Arith/Theory.lean

@@ -89,7 +89,7 @@ lemma mul_ext {a₁ a₂ b₁ b₂ : M} (ha : eql a₁ a₂) (hb : eql b₁ b₂
   have := by simpa [operator_eq_eq] using ModelsTheory.models M (Theory.CobhamR0'.replace “x. &0 * &1 = &2 * x”) (a₁ :>ₙ b₁ :>ₙ fun _ ↦ a₂)
   exact this b₁ b₂ hb e
 
-noncomputable instance : 𝐄𝐐 ≼ 𝐑₀' := System.Subtheory.ofAxm! <| by {
+noncomputable instance : 𝐄𝐐 ⪯ 𝐑₀' := Entailment.WeakerThan.ofAxm! <| by {
   intro φ hp
   cases hp
   · apply complete (consequence_iff.mpr fun M _ _ s f ↦ ?_)
@@ -141,29 +141,29 @@ noncomputable instance : 𝐄𝐐 ≼ 𝐑₀' := System.Subtheory.ofAxm! <| by
 
 open LO.Arith
 
-noncomputable instance CobhamR0'.subtheoryOfCobhamR0 : 𝐑₀' ≼ 𝐑₀ := System.Subtheory.ofAxm! <| by
+noncomputable instance CobhamR0'.subtheoryOfCobhamR0 : 𝐑₀' ⪯ 𝐑₀ := Entailment.WeakerThan.ofAxm! <| by
   intro φ hp
   rcases hp
   · apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff]
   · apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff]
-  case Ω₁ n m => exact System.by_axm _ (Theory.CobhamR0.Ω₁ n m)
-  case Ω₂ n m => exact System.by_axm _ (Theory.CobhamR0.Ω₂ n m)
-  case Ω₃ n m h => exact System.by_axm _ (Theory.CobhamR0.Ω₃ n m h)
-  case Ω₄ n => exact System.by_axm _ (Theory.CobhamR0.Ω₄ n)
+  case Ω₁ n m => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₁ n m)
+  case Ω₂ n m => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₂ n m)
+  case Ω₃ n m h => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₃ n m h)
+  case Ω₄ n => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₄ n)
 
-variable {T : Theory ℒₒᵣ} [𝐑₀ ≼ T]
+variable {T : Theory ℒₒᵣ} [𝐑₀ ⪯ T]
 
 lemma add_cobhamR0' {φ} : T ⊢! φ ↔ T + 𝐑₀' ⊢! φ := by
   constructor
-  · intro h; exact System.wk! (by simp [Theory.add_def]) h
+  · intro h; exact Entailment.wk! (by simp [Theory.add_def]) h
   · intro h
-    exact System.StrongCut.cut!
+    exact Entailment.StrongCut.cut!
       (by
         rintro φ (hp | hp)
-        · exact System.by_axm _ hp
-        · have : 𝐑₀' ⊢! φ := System.by_axm _ hp
-          have : 𝐑₀ ⊢! φ := System.Subtheory.prf! this
-          exact System.Subtheory.prf! this) h
+        · exact Entailment.by_axm _ hp
+        · have : 𝐑₀' ⊢! φ := Entailment.by_axm _ hp
+          have : 𝐑₀ ⊢! φ := Entailment.WeakerThan.pbl this
+          exact Entailment.WeakerThan.pbl this) h
 
 end Arith