chore(FirstOrder): rename to 𝐄𝐐

FormalMathematicsLab · Apr 4, 2024 · 00a81cf · 00a81cf
1 parent d7ee5af
commit 00a81cf
Show file tree

Hide file tree

Showing 13 changed files with 33 additions and 34 deletions.
diff --git a/Logic/FirstOrder/Arith/Basic.lean b/Logic/FirstOrder/Arith/Basic.lean
@@ -152,7 +152,7 @@ lemma consistent_of_sound [SoundOn T F] (hF : F ⊥) : System.Consistent T :=
 
 end
 
-variable {L : Language} [L.ORing] (T : Theory L) [𝐄𝐪 ≾ T]
+variable {L : Language} [L.ORing] (T : Theory L) [𝐄𝐐 ≾ T]
 
 lemma consequence_of (σ : Sentence L)
   (H : ∀ (M : Type u)

diff --git a/Logic/FirstOrder/Arith/EA/Basic.lean b/Logic/FirstOrder/Arith/EA/Basic.lean
@@ -4,7 +4,7 @@ namespace LO.FirstOrder
 
 namespace Arith
 
-variable {L : Language} [L.ORing] (T : Theory L) [𝐄𝐪 ≾ T] [L.Exp]
+variable {L : Language} [L.ORing] (T : Theory L) [𝐄𝐐 ≾ T] [L.Exp]
 
 instance : Language.ORing ℒₒᵣ(exp) := Language.ORing.mk
 

diff --git a/Logic/FirstOrder/Arith/Model.lean b/Logic/FirstOrder/Arith/Model.lean
@@ -200,7 +200,7 @@ abbrev Theory.trueArith : Theory ℒₒᵣ := Structure.theory ℒₒᵣ ℕ
 
 notation "𝐓𝐀" => Theory.trueArith
 
-variable (T : Theory ℒₒᵣ) [𝐄𝐪 ≾ T]
+variable (T : Theory ℒₒᵣ) [𝐄𝐐 ≾ T]
 
 lemma oRing_consequence_of (σ : Sentence ℒₒᵣ)
   (H : ∀ (M : Type)

diff --git a/Logic/FirstOrder/Arith/Nonstandard.lean b/Logic/FirstOrder/Arith/Nonstandard.lean
@@ -14,7 +14,7 @@ local notation "ℒₒᵣ⋆" => withStar
 def starUnbounded (c : ℕ) : Theory ℒₒᵣ⋆ := Set.range fun n : Fin c ↦ “!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆”
 
 def trueArithWithStarUnbounded (n : ℕ) : Theory ℒₒᵣ⋆ :=
-  𝐄𝐪 ∪ (Semiformula.lMap (Language.Hom.add₁ _ _) '' 𝐓𝐀) ∪ starUnbounded n
+  𝐄𝐐 ∪ (Semiformula.lMap (Language.Hom.add₁ _ _) '' 𝐓𝐀) ∪ starUnbounded n
 
 lemma trueArithWithStarUnbounded.cumulative : Cumulative trueArithWithStarUnbounded := fun c =>
   Set.union_subset_union_right _ <|
@@ -42,7 +42,7 @@ lemma satisfiable_union_trueArithWithStarUnbounded :
   (Compact.compact_cumulative trueArithWithStarUnbounded.cumulative).mpr
     satisfiable_trueArithWithStarUnbounded
 
-instance trueArithWithStarUnbounded.eqTheory : 𝐄𝐪 ≾ (⋃ c, trueArithWithStarUnbounded c) :=
+instance trueArithWithStarUnbounded.eqTheory : 𝐄𝐐 ≾ (⋃ c, trueArithWithStarUnbounded c) :=
   System.Subtheory.ofSubset <|
     Set.subset_iUnion_of_subset 0 (Set.subset_union_of_subset_left (Set.subset_union_left _ _) _)
 

diff --git a/Logic/FirstOrder/Arith/PeanoMinus.lean b/Logic/FirstOrder/Arith/PeanoMinus.lean
@@ -209,7 +209,7 @@ lemma pval_of_pval_nat_of_sigma_one : ∀ {n} {σ : Semisentence ℒₒᵣ n},
 
 end Model
 
-variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T]
+variable {T : Theory ℒₒᵣ} [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T]
 
 theorem sigma_one_completeness {σ : Sentence ℒₒᵣ} (hσ : Hierarchy Σ 1 σ) :
     ℕ ⊧ₘ σ → T ⊢ σ := fun H =>

diff --git a/Logic/FirstOrder/Arith/Representation.lean b/Logic/FirstOrder/Arith/Representation.lean
@@ -142,7 +142,7 @@ lemma codeOfPartrec_spec {k} {f : Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {
     exact ⟨c, models_code hc⟩
   exact Classical.epsilon_spec this y v
 
-variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
+variable {T : Theory ℒₒᵣ} [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
 
 section representation
 

diff --git a/Logic/FirstOrder/Basic/Eq.lean b/Logic/FirstOrder/Basic/Eq.lean
@@ -50,7 +50,7 @@ inductive eqAxiom : Theory L
   | relExt {k} (r : L.Rel k) :
     eqAxiom “∀* (!(Semiformula.vecEq varSumInL varSumInR) → !(Semiformula.rel r varSumInL) → !(Semiformula.rel r varSumInR))”
 
-notation "𝐄𝐪" => eqAxiom
+notation "𝐄𝐐" => eqAxiom
 
 end Eq
 
@@ -60,9 +60,7 @@ namespace Structure
 
 namespace Eq
 
-
-
-@[simp] lemma models_eqAxiom {M : Type u} [Nonempty M] [Structure L M] [Structure.Eq L M] : M ⊧ₘ* (𝐄𝐪 : Theory L) := ⟨by
+@[simp] lemma models_eqAxiom {M : Type u} [Nonempty M] [Structure L M] [Structure.Eq L M] : M ⊧ₘ* (𝐄𝐐 : Theory L) := ⟨by
   intro σ h
   cases h <;> simp[models_def, Semiformula.vecEq, Semiterm.val_func]
   · intro e h; congr; funext i; exact h i
@@ -71,15 +69,15 @@ namespace Eq
 
 variable (L)
 
-instance models_eqAxiom' (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M] : M ⊧ₘ* (𝐄𝐪 : Theory L) := Structure.Eq.models_eqAxiom
+instance models_eqAxiom' (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M] : M ⊧ₘ* (𝐄𝐐 : Theory L) := Structure.Eq.models_eqAxiom
 
 variable {M : Type u} [Nonempty M] [Structure L M]
 
 def eqv (a b : M) : Prop := (@Semiformula.Operator.Eq.eq L _).val ![a, b]
 
 variable {L}
 
-variable (H : M ⊧ₘ* (𝐄𝐪 : Theory L))
+variable (H : M ⊧ₘ* (𝐄𝐐 : Theory L))
 
 open Semiterm Theory Semiformula
 
@@ -123,7 +121,7 @@ lemma eqv_equivalence : Equivalence (eqv L (M := M)) where
   symm := eqv_symm H
   trans := eqv_trans H
 
-def eqvSetoid (H : M ⊧ₘ* (𝐄𝐪 : Theory L)) : Setoid M := Setoid.mk (eqv L) (eqv_equivalence H)
+def eqvSetoid (H : M ⊧ₘ* (𝐄𝐐 : Theory L)) : Setoid M := Setoid.mk (eqv L) (eqv_equivalence H)
 
 def QuotEq := Quotient (eqvSetoid H)
 
@@ -195,41 +193,41 @@ end Eq
 
 end Structure
 
-lemma consequence_iff_eq {T : Theory L} [𝐄𝐪 ≾ T] {σ : Sentence L} :
+lemma consequence_iff_eq {T : Theory L} [𝐄𝐐 ≾ T] {σ : Sentence L} :
     T ⊨ σ ↔ (∀ (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) := by
   simp[consequence_iff]; constructor
   · intro h M x s _ hM; exact h M x hM
   · intro h M x s hM
     haveI : Nonempty M := ⟨x⟩
-    have H : M ⊧ₘ* (𝐄𝐪 : Theory L) := Sound.modelsTheory_of_subtheory hM
+    have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := Sound.modelsTheory_of_subtheory hM
     have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
     exact e.models.mp $ h (Structure.Eq.QuotEq H) ⟦x⟧ (e.modelsTheory.mpr hM)
 
-lemma consequence_iff_eq' {T : Theory L} [𝐄𝐪 ≾ T] {σ : Sentence L} :
+lemma consequence_iff_eq' {T : Theory L} [𝐄𝐐 ≾ T] {σ : Sentence L} :
     T ⊨ σ ↔ (∀ (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M] [M ⊧ₘ* T], M ⊧ₘ σ) := by
   rw [consequence_iff_eq]
 
 lemma consequence_iff_add_eq {T : Theory L} {σ : Sentence L} :
-    T + 𝐄𝐪 ⊨ σ ↔ (∀ (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) :=
+    T + 𝐄𝐐 ⊨ σ ↔ (∀ (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) :=
   Iff.trans consequence_iff_eq (forall₄_congr <| fun M _ _ _ ↦ by simp)
 
-lemma satisfiableTheory_iff_eq {T : Theory L} [𝐄𝐪 ≾ T] :
+lemma satisfiableTheory_iff_eq {T : Theory L} [𝐄𝐐 ≾ T] :
     Semantics.SatisfiableTheory T ↔ (∃ (M : Type u) (_ : Nonempty M) (_ : Structure L M) (_ : Structure.Eq L M), M ⊧ₘ* T) := by
   simp[satisfiableTheory_iff]; constructor
   · intro ⟨M, x, s, hM⟩;
     haveI : Nonempty M := ⟨x⟩
-    have H : M ⊧ₘ* (𝐄𝐪 : Theory L) := Sound.modelsTheory_of_subtheory hM
+    have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := Sound.modelsTheory_of_subtheory hM
     have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
     exact ⟨Structure.Eq.QuotEq H, ⟦x⟧, inferInstance, inferInstance, e.modelsTheory.mpr hM⟩
   · intro ⟨M, i, s, _, hM⟩; exact ⟨M, i, s, hM⟩
 
-def ModelOfSatEq {T : Theory L} [𝐄𝐪 ≾ T] (sat : Semantics.SatisfiableTheory T) : Type _ :=
-  have H : ModelOfSat sat ⊧ₘ* (𝐄𝐪 : Theory L) := Sound.modelsTheory_of_subtheory (ModelOfSat.models sat)
+def ModelOfSatEq {T : Theory L} [𝐄𝐐 ≾ T] (sat : Semantics.SatisfiableTheory T) : Type _ :=
+  have H : ModelOfSat sat ⊧ₘ* (𝐄𝐐 : Theory L) := Sound.modelsTheory_of_subtheory (ModelOfSat.models sat)
   Structure.Eq.QuotEq H
 
 namespace ModelOfSatEq
 
-variable {T : Theory L} [𝐄𝐪 ≾ T] (sat : Semantics.SatisfiableTheory T)
+variable {T : Theory L} [𝐄𝐐 ≾ T] (sat : Semantics.SatisfiableTheory T)
 
 noncomputable instance : Nonempty (ModelOfSatEq sat) := Structure.Eq.QuotEq.inhabited _
 

diff --git a/Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean b/Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean
@@ -21,7 +21,7 @@ namespace Arith
 
 namespace FirstIncompleteness
 
-variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
+variable {T : Theory ℒₒᵣ} [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [DecidablePred T] [SigmaOneSound T] [Theory.Computable T]
 
 variable (T)
 
@@ -65,7 +65,7 @@ theorem main : ¬System.Complete T := System.incomplete_iff_exists_independent.m
 
 end FirstIncompleteness
 
-variable (T : Theory ℒₒᵣ) [DecidablePred T] [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T] [Theory.Computable T]
+variable (T : Theory ℒₒᵣ) [DecidablePred T] [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T] [Theory.Computable T]
 open FirstIncompleteness
 
 /- Gödel's First incompleteness theorem -/

diff --git a/Logic/FirstOrder/Incompleteness/SelfReference.lean b/Logic/FirstOrder/Incompleteness/SelfReference.lean
@@ -11,7 +11,7 @@ namespace Arith
 
 namespace SelfReference
 
-variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T]
+variable {T : Theory ℒₒᵣ} [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T]
 
 open Encodable Semiformula
 
@@ -65,7 +65,7 @@ end SelfReference
 
 namespace FirstIncompletenessBySelfReference
 
-variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T]
+variable {T : Theory ℒₒᵣ} [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T]
 
 section ProvableSentence
 

diff --git a/Logic/FirstOrder/Interpretation.lean b/Logic/FirstOrder/Interpretation.lean
@@ -11,9 +11,9 @@ structure Interpretation {L : Language} [L.Eq] (T : Theory L) (L' : Language) wh
   rel {k} : L'.Rel k → Semisentence L k
   func {k} : L'.Func k → Semisentence L (k + 1)
   domain_nonempty :
-    T + 𝐄𝐪 ⊨ ∃' domain
+    T + 𝐄𝐐 ⊨ ∃' domain
   func_defined {k} (f : L'.Func k) :
-    T + 𝐄𝐪 ⊨ ∀* ((Matrix.conj fun i ↦ domain/[#i]) ⟶ ∃'! (domain/[#0] ⋏ func f))
+    T + 𝐄𝐐 ⊨ ∀* ((Matrix.conj fun i ↦ domain/[#i]) ⟶ ∃'! (domain/[#0] ⋏ func f))
 
 namespace Interpretation
 

diff --git a/Logic/FirstOrder/Order/Le.lean b/Logic/FirstOrder/Order/Le.lean
@@ -66,7 +66,7 @@ end
 end Semiformula
 
 namespace Order
-variable {T : Theory L} [𝐄𝐪 ≾ T]
+variable {T : Theory L} [𝐄𝐐 ≾ T]
 
 noncomputable def leIffEqOrLt : T ⊢ “∀ ∀ (#0 ≤ #1 ↔ #0 = #1 ∨ #0 < #1)” :=
   Complete.complete

diff --git a/Logic/Summary.lean b/Logic/Summary.lean
@@ -62,7 +62,7 @@ noncomputable example {σ : Sentence L} : T ⊨ σ → T ⊢ σ := FirstOrder.co
 open Arith FirstIncompleteness
 
 variable (T : Theory ℒₒᵣ) [DecidablePred T]
-  [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T] [Theory.Computable T]
+  [𝐄𝐐 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T] [Theory.Computable T]
 
 /-- Gödel's first incompleteness theorem -/
 example : ¬System.Complete T :=

diff --git a/README.md b/README.md
@@ -126,7 +126,8 @@ The key results are summarised in `Logic/Summary.lean`.
 | :----:                              | ----                                           | ----                       | :----:   |
 | $(\rm Cut)\vdash_\mathrm{T} \Gamma$ | Derivation in Tait-Calculus + Cut              | [LO.FirstOrder.Derivation](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Calculus.html#LO.FirstOrder.Derivation) | `⊢¹ Γ`   |
 | $M \models \sigma$                  | Tarski's truth definition condition            | [LO.FirstOrder.Models](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Semantics/Semantics.html#LO.FirstOrder.Models) | `M ⊧ₘ σ` |
-| $\mathbf{Eq}$                       | Axiom of equality                              | [LO.FirstOrder.Theory.Eq](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Eq.html#LO.FirstOrder.Theory.Eq) | `𝐄𝐪` |
+| $T \triangleright U$                | Theory interpretation                          | [LO.FirstOrder.TheoryInterpretation](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Interpretation.html#LO.FirstOrder.TheoryInterpretation) | `T ⊳ U` |
+| $\mathbf{EQ}$                       | Axiom of equality                              | [LO.FirstOrder.Theory.eqAxiom](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Eq.html#LO.FirstOrder.Theory.eqAxiom) | `𝐄𝐐` |
 | $\mathbf{PA^-}$                     | Finitely axiomatized fragment of $\mathbf{PA}$ | [LO.FirstOrder.Arith.Theory.peanoMinus](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.peanoMinus) | `𝐏𝐀⁻` |
 | $\mathbf{I}_\mathrm{open}$          | Induction of open formula                      | [LO.FirstOrder.Arith.Theory.iOpen](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.iOpen) | `𝐈open` |
 | $\mathbf{I\Sigma}_n$                | Induction of $\Sigma_n$ formula                | [LO.FirstOrder.Arith.Theory.iSigma](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.iSigma) | `𝐈𝚺` |
@@ -168,7 +169,7 @@ The key results are summarised in `Logic/Summary.lean`.
   theorem LO.FirstOrder.Arith.first_incompleteness
       (T : LO.FirstOrder.Theory ℒₒᵣ)
       [DecidablePred T]
-      [𝐄𝐪 ≾ T]
+      [𝐄𝐐 ≾ T]
       [𝐏𝐀⁻ ≾ T]
       [LO.FirstOrder.Arith.SigmaOneSound T]
       [LO.FirstOrder.Theory.Computable T] :
@@ -179,7 +180,7 @@ The key results are summarised in `Logic/Summary.lean`.
     theorem LO.FirstOrder.Arith.undecidable
         (T : LO.FirstOrder.Theory ℒₒᵣ)
         [DecidablePred T]
-        [𝐄𝐪 ≾ T]
+        [𝐄𝐐 ≾ T]
         [𝐏𝐀⁻ ≾ T]
         [LO.FirstOrder.Arith.SigmaOneSound T]
         [LO.FirstOrder.Theory.Computable T] :