Foundation/Foundation/FirstOrder/Arithmetic/Basic/Model.lean at 67a8b2822db51ba0597abd8dec9310ead6ff2c56 · FormalizedFormalLogic/Foundation · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
module

public import Foundation.FirstOrder.Arithmetic.Basic.Misc

@[expose] public section
namespace LO.FirstOrder.Arithmetic

private lemma complete_aux (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Sentence ℒₒᵣ)
    (H : ∀ (M : Type w)
           [ORingStructure M]
           [Structure ℒₒᵣ M]
           [Structure.ORing ℒₒᵣ M]
           [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

section semantics

variable (M : Type*) [ORingStructure M]

instance standardModel : Structure ℒₒᵣ M where
  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 ↦
    match r with
    | ORing.Rel.eq => fun v ↦ v 0 = v 1
    | ORing.Rel.lt => fun v ↦ v 0 < v 1

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.Mul ℒₒᵣ M := ⟨fun _ _ ↦ rfl⟩

instance : Structure.Eq ℒₒᵣ 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 _ ↦
    match k, f with
    | _, Language.Zero.zero => by simp [Matrix.empty_eq]
    | _,   Language.One.one => by simp [Matrix.empty_eq]
    | _,   Language.Add.add => by simp
    | _,   Language.Mul.mul => by simp)
  (funext₃ fun k r _ =>
    match k, r with
    | _, Language.Eq.eq => by simp
    | _, Language.LT.lt => by simp)

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 :=
  standardModel_unique' M s hZero hOne hAdd hMul hEq hLT

end semantics

/-- 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 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 _ _ fun M _ _ ↦ Theory.Proof.sound h (H M)

end Arithmetic

class ArithmeticTheory.SoundOn (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop) where
  sound : ∀ {σ}, T ⊢ σ → F σ → ℕ↓[ℒₒᵣ] ⊧ σ

namespace ArithmeticTheory

variable (T : ArithmeticTheory) (F : Sentence ℒₒᵣ → Prop)

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

end ArithmeticTheory

end LO.FirstOrder