@@ -13,75 +13,30 @@ First-order schema `Schema L` is defined as a set of propositions, which may con
1313
1414namespace LO.FirstOrder
1515
16- structure Schema (L : Language) where
17- Mem : Proposition L → Prop
16+ abbrev Schema (L : Language) := Set (Proposition L)
1817
1918abbrev Theory (L : Language) := Set (Sentence L)
2019
2120namespace Schema
2221
2322variable {L : Language}
2423
25- instance : SetLike (Schema L) (Proposition L) where
26- coe 𝓢 := { φ | 𝓢.Mem φ }
27- coe_injective' := by
28- rintro ⟨⟩ ⟨⟩ _
29- congr
30-
31- lemma mem_def (𝓢 : Schema L) (φ : Proposition L) : 𝓢.Mem φ ↔ φ ∈ 𝓢 := Iff.rfl
32-
33- @[simp] lemma mem_mk_iff (φ : Proposition L) (P : Proposition L → Prop ) : φ ∈ Schema.mk P ↔ P φ := Iff.rfl
34-
35- lemma le_def (𝓢₁ 𝓢₂ : Schema L) : 𝓢₁ ≤ 𝓢₂ ↔ ∀ φ, φ ∈ 𝓢₁ → φ ∈ 𝓢₂ := Iff.rfl
36-
37- instance : CompleteLattice (Schema L) where
38- sup 𝓢₁ 𝓢₂ := ⟨fun φ ↦ φ ∈ 𝓢₁ ∨ φ ∈ 𝓢₂⟩
39- le_sup_left _ _ := by simp [le_def]; grind
40- le_sup_right _ _ := by simp [le_def]; grind
41- sup_le _ _ _ := by simp [le_def]; grind
42- inf 𝓢₁ 𝓢₂ := ⟨fun φ ↦ φ ∈ 𝓢₁ ∧ φ ∈ 𝓢₂⟩
43- inf_le_left _ _ := by simp [le_def]; grind
44- inf_le_right _ _ := by simp [le_def]
45- le_inf _ _ _ := by simp [le_def]; grind
46- sSup s := ⟨fun φ ↦ ∃ 𝓢 ∈ s, φ ∈ 𝓢⟩
47- le_sSup _ _ := by simp [le_def]; grind
48- sSup_le _ _ := by simp [le_def]; grind
49- sInf s := ⟨fun φ ↦ ∀ 𝓢 ∈ s, φ ∈ 𝓢⟩
50- sInf_le _ _ := by simp [le_def]; grind
51- le_sInf _ _ := by simp [le_def]; grind
52- top := ⟨fun _ ↦ True⟩
53- le_top _ _ := by simp
54- bot := ⟨fun _ ↦ False⟩
55- bot_le _ _ := by simp
56-
57- @[simp] lemma mem_sup_iff (𝓢₁ 𝓢₂ : Schema L) (φ : Proposition L) : φ ∈ 𝓢₁ ⊔ 𝓢₂ ↔ φ ∈ 𝓢₁ ∨ φ ∈ 𝓢₂ := Iff.rfl
58-
59- @[simp] lemma mem_inf_iff (𝓢₁ 𝓢₂ : Schema L) (φ : Proposition L) : φ ∈ 𝓢₁ ⊓ 𝓢₂ ↔ φ ∈ 𝓢₁ ∧ φ ∈ 𝓢₂ := Iff.rfl
60-
61- @[simp] lemma mem_sSup_iff (s : Set (Schema L)) (φ : Proposition L) : φ ∈ sSup s ↔ ∃ 𝓢 ∈ s, φ ∈ 𝓢 := Iff.rfl
62-
63- @[simp] lemma mem_sInf_iff (s : Set (Schema L)) (φ : Proposition L) : φ ∈ sInf s ↔ ∀ 𝓢 ∈ s, φ ∈ 𝓢 := Iff.rfl
64-
65- @[simp] lemma mem_top (φ : Proposition L) : φ ∈ (⊤ : Schema L) := by trivial
66-
67- @[simp] lemma not_mem_bot (φ : Proposition L) : φ ∉ (⊥ : Schema L) := by rintro ⟨⟩
68-
69- @[coe] def ofProposition (φ : Proposition L) : Schema L := ⟨(· = φ)⟩
24+ @[coe] def ofProposition (φ : Proposition L) : Schema L := {φ}
7025
7126instance : Coe (Proposition L) (Schema L) := ⟨fun φ ↦ ofProposition φ⟩
7227
7328@[simp] lemma mem_coe (φ ψ : Proposition L) : ψ ∈ (φ : Schema L) ↔ ψ = φ := by rfl
7429
7530instance : AdjunctiveSet (Proposition L) (Schema L) where
76- Subset 𝓢₁ 𝓢 ₂ := 𝓢 ₁ ≤ 𝓢 ₂
31+ Subset 𝔖₁ 𝔖 ₂ := 𝔖 ₁ ≤ 𝔖 ₂
7732 emptyCollection := ⊥
78- adjoin φ 𝓢 := φ ⊔ 𝓢
79- subset_iff := by simp [le_def ]
33+ adjoin φ 𝔖 := φ ⊔ 𝔖
34+ subset_iff := by simp [Set.subset_def ]
8035 not_mem_empty _ := by simp
8136 mem_cons_iff := by simp
8237
83- class IsClosed (𝓢 : Schema L) : Prop where
84- closed : ∀ ω : Rew L ℕ 0 ℕ 0 , ∀ φ ∈ 𝓢 , ω ▹ φ ∈ 𝓢
38+ class IsClosed (𝔖 : Schema L) : Prop where
39+ closed : ∀ ω : Rew L ℕ 0 ℕ 0 , ∀ φ ∈ 𝔖 , ω ▹ φ ∈ 𝔖
8540
8641namespace IsClosed
8742
@@ -91,27 +46,27 @@ instance : IsClosed (⊤ : Schema L) where
9146instance : IsClosed (⊥ : Schema L) where
9247 closed _ _ := by rintro ⟨⟩
9348
94- instance sup (𝓢₁ 𝓢 ₂ : Schema L) [IsClosed 𝓢 ₁] [IsClosed 𝓢 ₂] : IsClosed (𝓢₁ ⊔ 𝓢 ₂) where
49+ instance sup (𝔖₁ 𝔖 ₂ : Schema L) [IsClosed 𝔖 ₁] [IsClosed 𝔖 ₂] : IsClosed (𝔖₁ ∪ 𝔖 ₂) where
9550 closed ω φ h := by
96- have : φ ∈ 𝓢 ₁ ∨ φ ∈ 𝓢 ₂ := by simpa using h
51+ have : φ ∈ 𝔖 ₁ ∨ φ ∈ 𝔖 ₂ := by simpa using h
9752 rcases this with (h |h )
9853 · left; apply IsClosed.closed ω φ h
9954 · right; apply IsClosed.closed ω φ h
10055
101- instance inf (𝓢₁ 𝓢 ₂ : Schema L) [IsClosed 𝓢 ₁] [IsClosed 𝓢 ₂] : IsClosed (𝓢₁ ⊓ 𝓢 ₂) where
56+ instance inf (𝔖₁ 𝔖 ₂ : Schema L) [IsClosed 𝔖 ₁] [IsClosed 𝔖 ₂] : IsClosed (𝔖₁ ∩ 𝔖 ₂) where
10257 closed ω φ h := by
103- have : φ ∈ 𝓢 ₁ ∧ φ ∈ 𝓢 ₂ := by simpa using h
58+ have : φ ∈ 𝔖 ₁ ∧ φ ∈ 𝔖 ₂ := by simpa using h
10459 rcases this with ⟨h₁, h₂⟩
10560 constructor
10661 · apply IsClosed.closed ω φ h₁
10762 · apply IsClosed.closed ω φ h₂
10863
109- lemma sSup (s : Set (Schema L)) (H : ∀ 𝓢 ∈ s, IsClosed 𝓢 ) : IsClosed (sSup s) where
64+ lemma sSup (s : Set (Schema L)) (H : ∀ 𝔖 ∈ s, IsClosed 𝔖 ) : IsClosed (sSup s) where
11065 closed ω φ h := by
111- have : ∃ 𝓢 ∈ s, φ ∈ 𝓢 := by simpa using h
112- rcases this with ⟨𝓢 , hs, hφ⟩
113- have : IsClosed 𝓢 := H 𝓢 hs
114- exact ⟨𝓢 , hs, IsClosed.closed _ _ hφ⟩
66+ have : ∃ 𝔖 ∈ s, φ ∈ 𝔖 := by simpa using h
67+ rcases this with ⟨𝔖 , hs, hφ⟩
68+ have : IsClosed 𝔖 := H 𝔖 hs
69+ exact ⟨𝔖 , hs, IsClosed.closed _ _ hφ⟩
11570
11671instance sentence (σ : Sentence L) : IsClosed (σ : Schema L) where
11772 closed _ φ h := by
@@ -121,25 +76,25 @@ instance sentence (σ : Sentence L) : IsClosed (σ : Schema L) where
12176
12277end IsClosed
12378
124- @[coe] def uniClosure (𝓢 : Schema L) : Theory L := Set.image Semiformula.univCl {φ | φ ∈ 𝓢 }
79+ @[coe] def uniClosure (𝔖 : Schema L) : Theory L := Set.image Semiformula.univCl {φ | φ ∈ 𝔖 }
12580
12681instance : Coe (Schema L) (Theory L) := ⟨uniClosure⟩
12782
128- variable {𝓢 : Schema L}
83+ variable {𝔖 : Schema L}
12984
13085@[simp] lemma mem_uniClosure :
131- σ ∈ (𝓢 : Theory L) ↔ ∃ φ ∈ 𝓢 , Semiformula.univCl φ = σ := by simp [uniClosure]
86+ σ ∈ (𝔖 : Theory L) ↔ ∃ φ ∈ 𝔖 , Semiformula.univCl φ = σ := by simp [uniClosure]
13287
133- @[simp] lemma coe_sup (𝓢₁ 𝓢 ₂ : Schema L) : ((𝓢₁ ⊔ 𝓢 ₂ : Schema L) : Theory L) = (𝓢 ₁ : Theory L) ∪ (𝓢 ₂ : Theory L) := by
88+ @[simp] lemma coe_sup (𝔖₁ 𝔖 ₂ : Schema L) : ((𝔖₁ ∪ 𝔖 ₂ : Schema L) : Theory L) = (𝔖 ₁ : Theory L) ∪ (𝔖 ₂ : Theory L) := by
13489 ext σ; simp [uniClosure]; grind
13590
136- @[simp] lemma coe_sSup (s : Set (Schema L)) : ((sSup s : Schema L) : Theory L) = ⋃ 𝓢 ∈ s, (𝓢 : Theory L) := by
91+ @[simp] lemma coe_sSup (s : Set (Schema L)) : ((sSup s : Schema L) : Theory L) = ⋃ 𝔖 ∈ s, (𝔖 : Theory L) := by
13792 ext σ; simp [uniClosure, sSup]; grind
13893
13994@[simp] lemma coe_coe_proposition (φ : Proposition L) : ((φ : Schema L) : Theory L) = {φ.univCl} := by
14095 ext σ; simp [uniClosure]
14196
142- @ [grind <-] lemma coe_subset_coe_of_le {𝓢₁ 𝓢 ₂ : Schema L} (h : 𝓢 ₁ ≤ 𝓢 ₂) : (𝓢 ₁ : Theory L) ⊆ (𝓢 ₂ : Theory L) :=
97+ @ [grind <-] lemma coe_subset_coe_of_le {𝔖₁ 𝔖 ₂ : Schema L} (h : 𝔖 ₁ ≤ 𝔖 ₂) : (𝔖 ₁ : Theory L) ⊆ (𝔖 ₂ : Theory L) :=
14398 Set.image_mono h
14499
145100end Schema
0 commit comments