genericFillter

Author: iehality

Foundation/FirstOrder/Completeness/CanonicalModel.lean

@@ -468,6 +468,10 @@ lemma dn_neg_iff {φ : Proposition L} {p : ℙ⁻} : p ⊩ᶜ ∼φ ↔ p ⊩ 
   have := by simpa using (sound_minimal (Derivation.neg_doubleNegation φ) p)
   exact (this p (by simp)).symm
 
+@[simp] lemma verum (p : ℙ⁻) : p ⊩ᶜ ⊤ := by simp [iff_isForced, IsForced.not]
+
+@[simp] lemma falsum (p : ℙ⁻) : ¬p ⊩ᶜ ⊥ := by simp [iff_isForced]
+
 lemma not {φ : Proposition L} {p : ℙ⁻} : p ⊩ᶜ ∼φ ↔ ∀ q ≤ p, ¬q ⊩ᶜ φ := by
   simp [IsForced.not, dn_neg_iff,]; rfl
 
@@ -483,6 +487,12 @@ lemma not {φ : Proposition L} {p : ℙ⁻} : p ⊩ᶜ ∼φ ↔ ∀ q ≤ p, ¬
 @[simp] lemma exs {φ : Semiproposition L 1} {p : ℙ⁻} : p ⊩ᶜ ∃⁰ φ ↔ ∀ q ≤ p, ∃ r ≤ q, ∃ t, r ⊩ᶜ φ/[t] := by
   simp [iff_isForced, IsForced.not, Semiformula.subst_doubleNegation]; grind
 
+lemma monotone {φ : Proposition L} {p q : ℙ⁻} (h : q ≤ p) : p ⊩ᶜ φ → q ⊩ᶜ φ := IsForced.monotone h
+
+lemma gnericity {φ : Proposition L} {p : ℙ⁻} : p ⊩ᶜ φ ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ := calc
+  p ⊩ᶜ φ ↔ p ⊩ᶜ ∼∼φ := by simp
+  _      ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ := by rw [not]; simp [not]
+
 lemma complete {φ : Proposition L} : ℙ⁻ ∀⊩ᶜ φ ↔ 𝐋𝐊¹ ⊢ φ := by
   constructor
   · intro h

Foundation/FirstOrder/Completeness/CounterModel.lean

@@ -0,0 +1,68 @@
+module
+
+public import Foundation.FirstOrder.Completeness.CanonicalModel
+public import Foundation.Vorspiel.Order.Dense
+public import Mathlib.Logic.Equiv.List
+public import Mathlib.Logic.Encodable.Basic
+
+@[expose] public section
+
+namespace LO.FirstOrder.Derivation.Canonical
+
+open Order
+
+variable {L : Language}
+
+local notation "ℙ" => Sequent L
+local notation "ℙ⁻" => ConsistentSequent L
+
+scoped notation "ℍ" => LowerSet ℙ⁻
+
+instance [L.Encodable] [L.DecidableEq] : Encodable (Sequent L) := List.encodable
+
+open Classical in
+noncomputable instance [L.Encodable] : Encodable ℙ⁻ := Subtype.encodable
+
+def value (φ : Proposition L) : ℍ where
+  carrier := { p | p ⊩ᶜ φ }
+  lower'  _ _ hqp hp := IsWeaklyForced.monotone hqp hp
+
+notation "‖" φ "‖" => value φ
+
+lemma provable_iff_dense {φ : Proposition L} :
+    𝐋𝐊¹ ⊢ φ ↔ IsDense (‖φ‖ : Set ℙ⁻) := calc
+  𝐋𝐊¹ ⊢ φ ↔ ℙ⁻ ∀⊩ᶜ φ := IsWeaklyForced.complete.symm
+  _      ↔ IsDense (‖φ‖ : Set ℙ⁻) := by
+    constructor
+    · intro h p
+      suffices ∃ q ≤ p, q ⊩ᶜ φ by simpa [value]
+      refine ⟨p, by simp, h p⟩
+    · intro h p
+      apply IsWeaklyForced.gnericity.mpr
+      intro q hqp
+      simpa [value] using h q
+
+open Classical
+def decidablePoints (φ : Proposition L) : DenseSet ℙ⁻ where
+  set := {p | p ⊩ᶜ φ ∨ p ⊩ᶜ ∼φ}
+  is_dense := by
+    intro p
+    have : p ⊩ᶜ φ ⋎ ∼φ := IsWeaklyForced.complete.mpr Entailment.lem! p
+    have : ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ ∨ r ⊩ᶜ ∼φ := by simpa using this
+    simpa using this p (by rfl)
+
+variable [L.Encodable]
+
+theorem genericFIlter_exists (p : ℙ⁻) :
+    ∃ G : PFilter ℙ⁻, G.IsGeneric (Set.range decidablePoints) ∧ p ∈ G :=
+  PFilter.countable_isGeneric (Set.range decidablePoints) (Set.countable_range decidablePoints) p
+
+noncomputable def genericFilter (p : ℙ⁻) : PFilter ℙ⁻ := Classical.choose (genericFIlter_exists p)
+
+instance genericFilter_isGeneric (p : ℙ⁻) : (genericFilter p).IsGeneric (Set.range decidablePoints) :=
+  Classical.choose_spec (genericFIlter_exists p) |>.1
+
+@[simp] lemma mem_genericFilter (p : ℙ⁻) : p ∈ genericFilter p :=
+  Classical.choose_spec (genericFIlter_exists p) |>.2
+
+end LO.FirstOrder.Derivation.Canonical

Foundation/Vorspiel/Order/Dense.lean

@@ -99,30 +99,32 @@ def ofDescendingChain (s : ℕ → α) (hs : ∀ i j, i ≤ j → s i ≥ s j) :
 @[simp] lemma mem_descendingChain_iff (s : ℕ → α) (hs : ∀ i j, i ≤ j → s i ≥ s j) :
     x ∈ ofDescendingChain s hs ↔ ∃ i, s i ≤ x := by rfl
 
-class Generic (F : PFilter α) (𝓓 : Set (DenseSet α)) where
-  generic : ∀ d ∈ 𝓓, ∃ a ∈ F, a ∈ d
+class IsGeneric (F : PFilter α) (𝓓 : Set (DenseSet α)) where
+  isGeneric : ∀ d ∈ 𝓓, ∃ a ∈ F, a ∈ d
 
-@[simp] instance Generic.empty (F : PFilter α) : F.Generic ∅ := ⟨by simp⟩
+@[simp] instance IsGeneric.empty (F : PFilter α) : F.IsGeneric ∅ := ⟨by simp⟩
 
-theorem countable_generic [Inhabited α] (𝓓 : Set (DenseSet α)) (ctb : Set.Countable 𝓓) :
-    ∃ G, Generic G 𝓓 := by
+theorem countable_isGeneric (𝓓 : Set (DenseSet α)) (ctb : Set.Countable 𝓓) (a : α) :
+    ∃ G : PFilter α, G.IsGeneric 𝓓 ∧ a ∈ G := by
   by_cases emp : 𝓓.Nonempty
-  case neg => exact ⟨default, by simp [Set.not_nonempty_iff_eq_empty.mp emp]⟩
+  case neg => exact ⟨principal a, by simp [Set.not_nonempty_iff_eq_empty.mp emp]⟩
   have : ∃ D : ℕ → 𝓓, Function.Surjective D := ctb.exists_surjective emp
   rcases this with ⟨D, hD⟩
-  let s (n : ℕ) : α := n.rec default fun i ↦ (D i).val.choose
+  let s (n : ℕ) : α := n.rec a fun i ↦ (D i).val.choose
   have hs : ∀ i j, i ≤ j → s i ≥ s j := fun i j hij ↦
     Nat.monotone_of_succ_monotone (r := fun i j ↦ s i ≥ s j)
       (fun _ ↦ le_refl _)
       ⟨fun _ _ _ ↦ ge_trans⟩
       (by simp [s]) hij
-  refine ⟨ofDescendingChain s hs, ⟨?_⟩⟩
-  intro d hd
-  rcases show ∃ i, D i = ⟨d, hd⟩ from hD ⟨d, hd⟩ with ⟨i, hi⟩
-  refine ⟨s (i + 1), ?_, ?_⟩
-  · simp only [mem_descendingChain_iff]
-    exact ⟨i + 1, by rfl⟩
-  · simp [s, hi]
+  refine ⟨ofDescendingChain s hs, ⟨?_⟩, ?_⟩
+  · intro d hd
+    rcases show ∃ i, D i = ⟨d, hd⟩ from hD ⟨d, hd⟩ with ⟨i, hi⟩
+    refine ⟨s (i + 1), ?_, ?_⟩
+    · simp only [mem_descendingChain_iff]
+      exact ⟨i + 1, by rfl⟩
+    · simp [s, hi]
+  · suffices ∃ i, s i ≤ a by simpa
+    refine ⟨0, by simp [s]⟩
 
 end Order.PFilter