change(FirstOrder): redesign FirstOrder

Foundation.lean

@@ -42,6 +42,7 @@ public import Foundation.FirstOrder.Basic.BinderNotation
 public import Foundation.FirstOrder.Basic.Calculus
 public import Foundation.FirstOrder.Basic.Calculus2
 public import Foundation.FirstOrder.Basic.Coding
+public import Foundation.FirstOrder.Basic.CutFree
 public import Foundation.FirstOrder.Basic.Definability
 public import Foundation.FirstOrder.Basic.Eq
 public import Foundation.FirstOrder.Basic.Model
@@ -52,7 +53,6 @@ public import Foundation.FirstOrder.Basic.Semantics.Semantics
 public import Foundation.FirstOrder.Basic.Soundness
 public import Foundation.FirstOrder.Basic.Syntax.Formula
 public import Foundation.FirstOrder.Basic.Syntax.Rew
-public import Foundation.FirstOrder.Basic.Syntax.Theory
 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D1
 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D2
 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3
@@ -74,11 +74,10 @@ public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory
-public import Foundation.FirstOrder.Completeness.Coding
-public import Foundation.FirstOrder.Completeness.Completeness
-public import Foundation.FirstOrder.Completeness.Corollaries
-public import Foundation.FirstOrder.Completeness.SearchTree
-public import Foundation.FirstOrder.Completeness.SubLanguage
+public import Foundation.FirstOrder.Completeness
+public import Foundation.FirstOrder.Completeness.CanonicalModel
+public import Foundation.FirstOrder.Completeness.CountableSublanguage
+public import Foundation.FirstOrder.Completeness.CounterModel
 public import Foundation.FirstOrder.Hauptsatz
 public import Foundation.FirstOrder.Incompleteness.Consistency
 public import Foundation.FirstOrder.Incompleteness.Dense
@@ -213,8 +212,6 @@ public import Foundation.Modal.Axioms
 public import Foundation.Modal.Boxdot.Basic
 public import Foundation.Modal.Boxdot.GLPoint3_GrzPoint3
 public import Foundation.Modal.Boxdot.GL_Grz
-public import Foundation.Modal.Boxdot.GL_S
-public import Foundation.Modal.Boxdot.Grz_S
 public import Foundation.Modal.Boxdot.Jerabek
 public import Foundation.Modal.Boxdot.K4_S4
 public import Foundation.Modal.Boxdot.Ver_Triv
@@ -350,7 +347,6 @@ public import Foundation.Modal.Logic.GLPlusBoxBot.Basic
 public import Foundation.Modal.Logic.GLPoint3OplusBoxBot.Basic
 public import Foundation.Modal.Logic.Global
 public import Foundation.Modal.Logic.S.Basic
-public import Foundation.Modal.Logic.S.Consistent
 public import Foundation.Modal.Logic.SumNormal
 public import Foundation.Modal.Logic.SumQuasiNormal
 public import Foundation.Modal.LogicSymbol
@@ -380,7 +376,6 @@ public import Foundation.Propositional.Boolean.NNFormula
 public import Foundation.Propositional.Boolean.Tait
 public import Foundation.Propositional.Boolean.ZeroSubst
 public import Foundation.Propositional.ConsistentTableau
-public import Foundation.Propositional.Decidable
 public import Foundation.Propositional.Dialectica.Basic
 public import Foundation.Propositional.Entailment.AxiomDNE
 public import Foundation.Propositional.Entailment.AxiomEFQ
@@ -463,20 +458,6 @@ public import Foundation.Propositional.Neighborhood.NB.Hilbert.WF
 public import Foundation.Propositional.Slash
 public import Foundation.Propositional.Tait.Calculus
 public import Foundation.Propositional.Translation
-public import Foundation.ProvabilityLogic.Arithmetic
-public import Foundation.ProvabilityLogic.Classification.LetterlessTrace
-public import Foundation.ProvabilityLogic.Classification.Result
-public import Foundation.ProvabilityLogic.Classification.Trace
-public import Foundation.ProvabilityLogic.GL.Completeness
-public import Foundation.ProvabilityLogic.GL.Soundness
-public import Foundation.ProvabilityLogic.GL.Uniform
-public import Foundation.ProvabilityLogic.GL.Unprovability
-public import Foundation.ProvabilityLogic.Grz.Completeness
-public import Foundation.ProvabilityLogic.N.Soundness
-public import Foundation.ProvabilityLogic.Realization
-public import Foundation.ProvabilityLogic.S.Completeness
-public import Foundation.ProvabilityLogic.S.Soundness
-public import Foundation.ProvabilityLogic.SolovaySentences
 public import Foundation.SecondOrder.Derivation
 public import Foundation.SecondOrder.Semantics
 public import Foundation.SecondOrder.Syntax.Formula
@@ -515,9 +496,13 @@ public import Foundation.Vorspiel.Nat.Basic
 public import Foundation.Vorspiel.Nat.Matrix
 public import Foundation.Vorspiel.NotationClass
 public import Foundation.Vorspiel.Option
-public import Foundation.Vorspiel.Order
+public import Foundation.Vorspiel.Order.Dense
+public import Foundation.Vorspiel.Order.Heyting
+public import Foundation.Vorspiel.Order.Ideal
+public import Foundation.Vorspiel.Order.Lattice
+public import Foundation.Vorspiel.Order.LowerSet
+public import Foundation.Vorspiel.Order.Regular
 public import Foundation.Vorspiel.Part
-public import Foundation.Vorspiel.Preorder
 public import Foundation.Vorspiel.Quotient
 public import Foundation.Vorspiel.Rel.Basic
 public import Foundation.Vorspiel.Rel.CWF

Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean

@@ -256,7 +256,7 @@ lemma sigma_of_sigma_ex {φ : Semiformula L ξ (n + 1)} : Hierarchy 𝚺 s (∃
 
 set_option linter.flexible false in
 lemma rew (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : Hierarchy Γ s φ → Hierarchy Γ s (ω ▹ φ) := by
-  intro h; induction h generalizing n₂ <;> try simp [*, Semiformula.rew_rel, Semiformula.rew_nrel]
+  intro h; induction h generalizing n₂ <;> try simp [*]
   case sigma ih => exact (ih _).accum _
   case pi ih => exact (ih _).accum _
   case dummy_pi ih => exact (ih _).dummy_pi
@@ -476,7 +476,7 @@ end Arithmetic
 abbrev ArithmeticTheory.SoundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) := T.SoundOn (Arithmetic.Hierarchy Γ k)
 
 lemma ArithmeticTheory.soundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) [T.SoundOnHierarchy Γ k] :
-    T ⊢ σ → Arithmetic.Hierarchy Γ k σ → ℕ ⊧ₘ σ := SoundOn.sound
+    T ⊢ σ → Arithmetic.Hierarchy Γ k σ → ℕ↓[ℒₒᵣ] ⊧ σ := SoundOn.sound
 
 instance (T : ArithmeticTheory) [T.SoundOnHierarchy 𝚺 1] : Entailment.Consistent T :=
   T.consistent_of_sound (Arithmetic.Hierarchy 𝚺 1) (by simp)

Foundation/FirstOrder/Arithmetic/Basic/Misc.lean

@@ -135,14 +135,12 @@ def bexsLTSucc (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)) : Semiformu
 
 variable {M : Type*} {s : Structure L M} [LT M] [One M] [Add M] [Structure.LT L M] [Structure.One L M] [Structure.Add L M]
 
-variable {t : Semiterm L ξ n} {φ : Semiformula L ξ (n + 1)}
-
-lemma eval_ballLTSucc {e ε} :
-    Eval s e ε (φ.ballLTSucc t) ↔ ∀ x < t.val s e ε + 1, Eval s (x :> e) ε φ := by
+lemma eval_ballLTSucc {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv bv} :
+    (φ.ballLTSucc t).Eval (M := M) fv bv ↔ ∀ x < t.val (M := M) fv bv + 1, φ.Eval (M := M) (x :> fv) bv := by
   simp [ballLTSucc, Semiterm.Operator.numeral]
 
-lemma eval_bexsLTSucc {e ε} :
-    Eval s e ε (φ.bexsLTSucc t) ↔ ∃ x < t.val s e ε + 1, Eval s (x :> e) ε φ := by
+lemma eval_bexsLTSucc {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} {fv bv} :
+    (φ.bexsLTSucc t).Eval (M := M) fv bv ↔ ∃ x < t.val (M := M) fv bv + 1, φ.Eval (M := M) (x :> fv) bv := by
   simp [bexsLTSucc, Semiterm.Operator.numeral]
 
 end Semiformula
@@ -167,8 +165,6 @@ macro_rules
 
 end BinderNotation
 
-abbrev ArithmeticTheory := Theory ℒₒᵣ
-
 end FirstOrder
 
 end LO

Foundation/FirstOrder/Arithmetic/Basic/Model.lean

@@ -5,15 +5,15 @@ public import Foundation.FirstOrder.Arithmetic.Basic.Misc
 @[expose] public section
 namespace LO.FirstOrder.Arithmetic
 
-private lemma consequence_of_aux (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ)
+private lemma complete_aux (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Sentence ℒₒᵣ)
     (H : ∀ (M : Type w)
            [ORingStructure M]
            [Structure ℒₒᵣ M]
            [Structure.ORing ℒₒᵣ M]
-           [M ⊧ₘ* T],
-           M ⊧ₘ φ) :
-    T ⊨ φ := consequence_iff_consequence.{_, w}.mp <| consequence_iff_eq.mpr fun M _ _ _ hT =>
-  letI : Structure.Model ℒₒᵣ M ⊧ₘ* T := Structure.ElementaryEquiv.modelsTheory.mp hT
+           [M↓[ℒₒᵣ] ⊧* T],
+           M↓[ℒₒᵣ] ⊧ φ) :
+    T ⊢ φ := Theory.Proof.complete <| consequence_iff_eq.mpr fun M _ _ _ hT ↦
+  letI : (Structure.Model ℒₒᵣ M)↓[ℒₒᵣ] ⊧* T := Structure.ElementaryEquiv.modelsTheory.mp hT
   Structure.ElementaryEquiv.models.mpr (H (Structure.Model ℒₒᵣ M))
 
 open Language
@@ -23,38 +23,40 @@ section semantics
 variable (M : Type*) [ORingStructure M]
 
 instance standardModel : Structure ℒₒᵣ M where
-  func := fun _ f =>
+  func := fun _ f ↦
     match f with
-    | ORing.Func.zero => fun _ => 0
-    |  ORing.Func.one => fun _ => 1
-    |  ORing.Func.add => fun v => v 0 + v 1
-    |  ORing.Func.mul => fun v => v 0 * v 1
-  rel := fun _ r =>
+    | ORing.Func.zero => fun _ ↦ 0
+    |  ORing.Func.one => fun _ ↦ 1
+    |  ORing.Func.add => fun v ↦ v 0 + v 1
+    |  ORing.Func.mul => fun v ↦ v 0 * v 1
+  rel := fun _ r ↦
     match r with
-    | ORing.Rel.eq => fun v => v 0 = v 1
-    | ORing.Rel.lt => fun v => v 0 < v 1
+    | ORing.Rel.eq => fun v ↦ v 0 = v 1
+    | ORing.Rel.lt => fun v ↦ v 0 < v 1
 
-instance : Structure.Eq ℒₒᵣ M :=
-  ⟨by intro a b; simp [standardModel, Semiformula.Operator.val, Semiformula.Operator.Eq.sentence_eq, Semiformula.eval_rel]⟩
+instance : Structure.Eq ℒₒᵣ M where
+  eq a b := by
+    unfold standardModel
+    simp [Semiformula.Operator.val, Semiformula.Operator.Eq.sentence_eq]
 
 instance : Structure.Zero ℒₒᵣ M := ⟨rfl⟩
 
 instance : Structure.One ℒₒᵣ M := ⟨rfl⟩
 
-instance : Structure.Add ℒₒᵣ M := ⟨fun _ _ => rfl⟩
+instance : Structure.Add ℒₒᵣ M := ⟨fun _ _ ↦ rfl⟩
 
-instance : Structure.Mul ℒₒᵣ M := ⟨fun _ _ => rfl⟩
+instance : Structure.Mul ℒₒᵣ M := ⟨fun _ _ ↦ rfl⟩
 
-instance : Structure.Eq ℒₒᵣ M := ⟨fun _ _ => iff_of_eq rfl⟩
+instance : Structure.Eq ℒₒᵣ M := ⟨fun _ _ ↦ iff_of_eq rfl⟩
 
-instance : Structure.LT ℒₒᵣ M := ⟨fun _ _ => iff_of_eq rfl⟩
+instance : Structure.LT ℒₒᵣ M := ⟨fun _ _ ↦ iff_of_eq rfl⟩
 
 instance : ORing ℒₒᵣ := ORing.mk
 
 lemma standardModel_unique' (s : Structure ℒₒᵣ M)
     (hZero : Structure.Zero ℒₒᵣ M) (hOne : Structure.One ℒₒᵣ M) (hAdd : Structure.Add ℒₒᵣ M) (hMul : Structure.Mul ℒₒᵣ M)
     (hEq : Structure.Eq ℒₒᵣ M) (hLT : Structure.LT ℒₒᵣ M) : s = standardModel M := Structure.ext
-  (funext₃ fun k f _ =>
+  (funext₃ fun k f _ ↦
     match k, f with
     | _, Language.Zero.zero => by simp [Matrix.empty_eq]
     | _,   Language.One.one => by simp [Matrix.empty_eq]
@@ -72,31 +74,29 @@ lemma standardModel_unique (s : Structure ℒₒᵣ M)
 
 end semantics
 
-lemma consequence_of_models (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M ⊧ₘ* T], M ⊧ₘ φ) :
-    T ⊨ φ := consequence_of_aux T φ fun M _ s _ _ ↦ by
+/-- provable_of_models -/
+lemma complete (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M↓[ℒₒᵣ] ⊧* T], M↓[ℒₒᵣ] ⊧ φ) :
+    T ⊢ φ := complete_aux T φ fun M _ s _ _ ↦ by
   rcases standardModel_unique M s
   exact H M
 
-lemma provable_of_models (T : ArithmeticTheory) [𝗘𝗤 ⪯ T] (φ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStructure M] [M ⊧ₘ* T], M ⊧ₘ φ) :
-    T ⊢ φ := complete <| consequence_of_models _ _ H
-
-lemma weakerThan_of_models (T S : ArithmeticTheory) [𝗘𝗤 ⪯ S]
+lemma weakerThan_of_models (T S : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ S]
     (H : ∀ (M : Type*)
            [ORingStructure M]
-           [M ⊧ₘ* S],
-           M ⊧ₘ* T) : T ⪯ S :=
-  Entailment.weakerThan_iff.mpr fun h ↦ complete <| consequence_of_models _ _ fun M _ _ ↦ sound! h (H M)
+           [M↓[ℒₒᵣ] ⊧* S],
+           M↓[ℒₒᵣ] ⊧* T) : T ⪯ S :=
+  Entailment.weakerThan_iff.mpr fun h ↦ complete _ _ fun M _ _ ↦ Theory.Proof.sound h (H M)
 
 end Arithmetic
 
 class ArithmeticTheory.SoundOn (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop) where
-  sound : ∀ {σ}, T ⊢ σ → F σ → ℕ ⊧ₘ σ
+  sound : ∀ {σ}, T ⊢ σ → F σ → ℕ↓[ℒₒᵣ] ⊧ σ
 
 namespace ArithmeticTheory
 
 variable (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop)
 
-instance [ℕ ⊧ₘ* T] : T.SoundOn F := ⟨fun b _ ↦ consequence_iff.mp (sound! b) ℕ inferInstance⟩
+instance [ℕ↓[ℒₒᵣ] ⊧* T] : T.SoundOn F := ⟨fun b _ ↦ consequence_iff.mp (Theory.Proof.sound b) ℕ inferInstance⟩
 
 lemma consistent_of_sound [SoundOn T F] (hF : F ⊥) : Entailment.Consistent T :=
   Entailment.consistent_iff_unprovable_bot.mpr fun b ↦ SoundOn.sound b hF

Foundation/FirstOrder/Arithmetic/Basic/Monotone.lean

@@ -14,9 +14,9 @@ namespace Monotone
 
 variable {L : Language} {M : Type*} [LE M] [Structure L M] [Monotone L M]
 
-lemma term_monotone (t : Semiterm L ξ n) {e₁ e₂ : Fin n → M} {ε₁ ε₂ : ξ → M}
-    (he : ∀ i, e₁ i ≤ e₂ i) (hε : ∀ i, ε₁ i ≤ ε₂ i) :
-    t.valm M e₁ ε₁ ≤ t.valm M e₂ ε₂ := by
+lemma term_monotone (t : Semiterm L ξ n) {fv₁ fv₂ : Fin n → M} {bv₁ bv₂ : ξ → M}
+    (he : ∀ i, fv₁ i ≤ fv₂ i) (hε : ∀ i, bv₁ i ≤ bv₂ i) :
+    t.val fv₁ bv₁ ≤ t.val fv₂ bv₂ := by
   induction t <;> simp [*, Semiterm.val_func, Monotone.monotone]
 
 end Monotone