feat(model_theory/terms_and_formulas): Define satisfiability and sema…

…ntic equivalence of formulas (#11928)

Defines satisfiability of theories
Provides a default model of a satisfiable theory
Defines semantic (logical) equivalence of formulas

src/model_theory/basic.lean

@@ -52,9 +52,9 @@ structure language :=
 namespace language
 
 /-- The empty language has no symbols. -/
-def empty : language := ⟨λ _, pempty, λ _, pempty⟩
+protected def empty : language := ⟨λ _, pempty, λ _, pempty⟩
 
-instance : inhabited language := ⟨empty⟩
+instance : inhabited language := ⟨language.empty⟩
 
 /-- The type of constants in a given language. -/
 @[nolint has_inhabited_instance] def const (L : language) := L.functions 0
@@ -77,8 +77,11 @@ instance is_relational_of_empty_functions {symb : ℕ → Type*} : is_relational
 instance is_algebraic_of_empty_relations {symb : ℕ → Type*}  : is_algebraic ⟨symb, λ _, pempty⟩ :=
 ⟨by { intro n, apply pempty.elim }⟩
 
-instance is_relational_empty : is_relational (empty) := language.is_relational_of_empty_functions
-instance is_algebraic_empty : is_algebraic (empty) := language.is_algebraic_of_empty_relations
+instance is_relational_empty : is_relational language.empty :=
+language.is_relational_of_empty_functions
+
+instance is_algebraic_empty : is_algebraic language.empty :=
+language.is_algebraic_of_empty_relations
 
 variables (L) (M : Type*)
 
@@ -130,6 +133,11 @@ instance : has_coe_t L.const M :=
 lemma fun_map_eq_coe_const {c : L.const} {x : fin 0 → M} :
   fun_map c x = c := congr rfl (funext fin.elim0)
 
+/-- Given a language with a nonempty type of constants, any structure will be nonempty. This cannot
+  be a global instance, because `L` becomes a metavariable. -/
+lemma nonempty_of_nonempty_constants [h : nonempty L.const] : nonempty M :=
+h.map coe
+
 namespace hom
 
 instance has_coe_to_fun : has_coe_to_fun (M →[L] N) (λ _, M → N) := ⟨to_fun⟩

src/model_theory/definability.lean

@@ -20,8 +20,6 @@ This file defines what it means for a set over a first-order structure to be def
 
 -/
 
-universes u v
-
 namespace first_order
 namespace language
 

src/model_theory/terms_and_formulas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Aaron Anderson, Jesse Michael Han, Floris van Doorn. All righ
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jesse Michael Han, Floris van Doorn
 -/
+import data.finset.basic
 import model_theory.basic
 
 /-!
@@ -16,7 +17,12 @@ This file defines first-order languages and structures in the style of the
 * A `first_order.language.formula` is defined so that `L.formula α` is the type of `L`-formulas with
   free variables indexed by `α`.
 * A `first_order.language.sentence` is a formula with no free variables.
-* A `first_order.language.theory` is a set of sentences.
+* A `first_order.language.Theory` is a set of sentences.
+* `first_order.language.Theory.is_satisfiable` indicates that a theory has a nonempty model.
+* Given a theory `T`, `first_order.language.Theory.semantically_equivalent` defines an equivalence
+relation `T.semantically_equivalent` on formulas of a particular signature, indicating that the
+formulas have the same realization in models of `T`. (This is more often known as logical
+equivalence once it is known that this is equivalent to the proof-theoretic definition.)
 
 ## References
 For the Flypitch project:
@@ -115,7 +121,7 @@ instance {α : Type} {n : ℕ} : inhabited (L.bounded_formula α n) :=
 @[reducible] def sentence           := L.formula pempty
 
 /-- A theory is a set of sentences. -/
-@[reducible] def theory := set L.sentence
+@[reducible] def Theory := set L.sentence
 
 variables {L} {α : Type}
 
@@ -125,8 +131,7 @@ variable {n : ℕ}
 @[simps] instance : has_bot (L.bounded_formula α n) := ⟨bd_falsum⟩
 
 /-- The negation of a bounded formula is also a bounded formula. -/
-@[reducible] def bd_not (φ : L.bounded_formula α n) : L.bounded_formula α n :=
-  bd_imp φ ⊥
+@[reducible] def bd_not (φ : L.bounded_formula α n) : L.bounded_formula α n := bd_imp φ ⊥
 
 @[simps] instance : has_top (L.bounded_formula α n) := ⟨bd_not bd_falsum⟩
 
@@ -160,7 +165,7 @@ end formula
 variable {L}
 
 instance nonempty_bounded_formula {α : Type} (n : ℕ) : nonempty $ L.bounded_formula α n :=
-  nonempty.intro (by constructor)
+nonempty.intro (by constructor)
 
 variables (M)
 
@@ -177,6 +182,16 @@ variables (M)
   realize_bounded_formula M (bd_not f) v xs = ¬ realize_bounded_formula M f v xs :=
 rfl
 
+lemma realize_inf {l} (φ ψ : L.bounded_formula α l) (v : α → M) (xs : fin l → M) :
+  realize_bounded_formula M (φ ⊓ ψ) v xs =
+    (realize_bounded_formula M φ v xs ∧ realize_bounded_formula M ψ v xs) :=
+by simp
+
+lemma realize_imp {l} (φ ψ : L.bounded_formula α l) (v : α → M) (xs : fin l → M) :
+  realize_bounded_formula M (φ.bd_imp ψ) v xs =
+    (realize_bounded_formula M φ v xs → realize_bounded_formula M ψ v xs) :=
+by simp only [realize_bounded_formula]
+
 /-- A bounded formula can be evaluated as true or false by giving values to each free variable. -/
 @[reducible] def realize_formula (f : L.formula α) (v : α → M) : Prop :=
 realize_bounded_formula M f v fin_zero_elim
@@ -185,8 +200,20 @@ realize_bounded_formula M f v fin_zero_elim
 @[reducible] def realize_sentence (φ : L.sentence) : Prop :=
 realize_formula M φ pempty.elim
 
+infix ` ⊨ `:51 := realize_sentence -- input using \|= or \vDash, but not using \models
+
+/-- A model of a theory is a structure in which every sentence is realized as true. -/
+@[reducible] def Theory.model (T : L.Theory) : Prop :=
+∀ φ ∈ T, realize_sentence M φ
+
+infix ` ⊨ `:51 := Theory.model -- input using \|= or \vDash, but not using \models
+
 variable {M}
 
+lemma Theory.model.mono {T T' : L.Theory} (h : T'.model M) (hs : T ⊆ T') :
+  T.model M :=
+λ φ hφ, h φ (hs hφ)
+
 @[simp] lemma realize_bounded_formula_relabel {α β : Type} {n : ℕ}
   (g : α → β) (v : β → M) (xs : fin n → M) (φ : L.bounded_formula α n) :
   realize_bounded_formula M (φ.relabel g) v xs ↔ realize_bounded_formula M φ (v ∘ g) xs :=
@@ -253,5 +280,139 @@ begin
   rw [fin.coe_nat_eq_last, fin.snoc_last],
 end
 
+namespace Theory
+
+/-- A theory is satisfiable if a structure models it. -/
+def is_satisfiable (T : L.Theory) : Prop :=
+∃ (M : Type (max u v)) [nonempty M] [str : L.Structure M], @Theory.model L M str T
+
+/-- A theory is finitely satisfiable if all of its finite subtheories are satisfiable. -/
+def is_finitely_satisfiable (T : L.Theory) : Prop :=
+∀ (T0 : finset L.sentence), (T0 : L.Theory) ⊆ T → (T0 : L.Theory).is_satisfiable
+
+/-- Given that a theory is satisfiable, selects a model using choice. -/
+def is_satisfiable.some_model {T : L.Theory} (h : T.is_satisfiable) : Type* := classical.some h
+
+instance is_satisfiable.nonempty_some_model {T : L.Theory} (h : T.is_satisfiable) :
+  nonempty (h.some_model) :=
+classical.some (classical.some_spec h)
+
+noncomputable instance is_satisfiable.inhabited_some_model {T : L.Theory} (h : T.is_satisfiable) :
+  inhabited (h.some_model) := classical.inhabited_of_nonempty'
+
+noncomputable instance is_satisfiable.some_model_structure {T : L.Theory} (h : T.is_satisfiable) :
+  L.Structure (h.some_model) :=
+classical.some (classical.some_spec (classical.some_spec h))
+
+lemma is_satisfiable.some_model_models {T : L.Theory} (h : T.is_satisfiable) :
+  T.model h.some_model :=
+classical.some_spec (classical.some_spec (classical.some_spec h))
+
+lemma model.is_satisfiable {T : L.Theory} (M : Type (max u v)) [n : nonempty M]
+  [S : L.Structure M] (h : T.model M) : T.is_satisfiable :=
+⟨M, n, S, h⟩
+
+lemma is_satisfiable.mono {T T' : L.Theory} (h : T'.is_satisfiable) (hs : T ⊆ T') :
+  T.is_satisfiable :=
+⟨h.some_model, h.nonempty_some_model, h.some_model_structure,
+  h.some_model_models.mono hs⟩
+
+lemma is_satisfiable.is_finitely_satisfiable {T : L.Theory} (h : T.is_satisfiable) :
+  T.is_finitely_satisfiable :=
+λ _, h.mono
+
+/-- A theory models a (bounded) formula when any of its nonempty models realizes that formula on all
+  inputs.-/
+def models_bounded_formula {n : ℕ} {α : Type} (T : L.Theory) (φ : L.bounded_formula α n) : Prop :=
+  ∀ (M : Type (max u v)) [nonempty M] [str : L.Structure M] (v : α → M) (xs : fin n → M),
+    @Theory.model L M str T → @realize_bounded_formula L M str α n φ v xs
+
+infix ` ⊨ `:51 := models_bounded_formula -- input using \|= or \vDash, but not using \models
+
+lemma models_formula_iff {α : Type} (T : L.Theory) (φ : L.formula α) :
+  T ⊨ φ ↔ ∀ (M : Type (max u v)) [nonempty M] [str : L.Structure M] (v : α → M),
+    @Theory.model L M str T → @realize_formula L M str α φ v :=
+begin
+  refine forall_congr (λ M, forall_congr (λ ne, forall_congr (λ str, forall_congr
+    (λ v, ⟨λ h, h fin_zero_elim, λ h xs, _⟩)))),
+  rw subsingleton.elim xs fin_zero_elim,
+  exact h,
+end
+
+lemma models_sentence_iff (T : L.Theory) (φ : L.sentence) :
+  T ⊨ φ ↔ ∀ (M : Type (max u v)) [nonempty M] [str : L.Structure M],
+    @Theory.model L M str T → @realize_sentence L M str φ :=
+begin
+  rw [models_formula_iff],
+  refine forall_congr (λ M, forall_congr (λ ne, forall_congr (λ str, _))),
+  refine ⟨λ h, h pempty.elim, λ h v, _⟩,
+  rw subsingleton.elim v pempty.elim,
+  exact h,
+end
+
+variable {n : ℕ}
+
+/-- Two (bounded) formulas are semantically equivalent over a theory `T` when they have the same
+interpretation in every model of `T`. (This is also known as logical equivalence, which also has a
+proof-theoretic definition.) -/
+def semantically_equivalent (T : L.Theory) (φ ψ : L.bounded_formula α n) : Prop :=
+T ⊨ (bd_imp φ ψ ⊓ bd_imp ψ φ)
+
+lemma semantically_equivalent.realize_eq {T : L.Theory} {φ ψ : L.bounded_formula α n}
+  {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] (hM : T.model M)
+  (h : T.semantically_equivalent φ ψ) :
+  realize_bounded_formula M φ = realize_bounded_formula M ψ :=
+funext (λ v, funext (λ xs, begin
+  have h' := h M v xs hM,
+  simp only [realize_bounded_formula, has_inf_inf, realize_not, not_forall, exists_prop, not_and,
+    not_not] at h',
+  exact iff_eq_eq.mp ⟨h'.1, h'.2⟩,
+end))
+
+lemma semantically_equivalent.some_model_realize_eq {T : L.Theory} {φ ψ : L.bounded_formula α n}
+  (hsat : T.is_satisfiable) (h : T.semantically_equivalent φ ψ) :
+  realize_bounded_formula (hsat.some_model) φ = realize_bounded_formula (hsat.some_model) ψ :=
+h.realize_eq hsat.some_model_models
+
+/-- Semantic equivalence forms an equivalence relation on formulas. -/
+def semantically_equivalent_setoid (T : L.Theory) : setoid (L.bounded_formula α n) :=
+{ r := semantically_equivalent T,
+  iseqv := ⟨λ φ M ne str v xs hM, by simp,
+    λ φ ψ h M ne str v xs hM, begin
+      haveI := ne,
+      have h := h M v xs hM,
+      rw [realize_inf, and_comm] at h,
+      rw realize_inf,
+      exact h,
+    end, λ φ ψ θ h1 h2 M ne str v xs hM, begin
+      haveI := ne,
+      have h1' := h1 M v xs hM,
+      have h2' := h2 M v xs hM,
+      rw [realize_inf, realize_imp, realize_imp] at *,
+      exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩,
+    end⟩ }
+
+lemma semantically_equivalent_not_not {T : L.Theory} {φ : L.bounded_formula α n} :
+  T.semantically_equivalent φ (bd_not (bd_not φ)) :=
+λ M ne str v xs hM, by simp
+
+lemma imp_semantically_equivalent_not_sup {T : L.Theory} {φ ψ : L.bounded_formula α n} :
+  T.semantically_equivalent (bd_imp φ ψ) (bd_not φ ⊔ ψ) :=
+λ M ne str v xs hM, by simp
+
+lemma sup_semantically_equivalent_not_inf_not {T : L.Theory} {φ ψ : L.bounded_formula α n} :
+  T.semantically_equivalent (φ ⊔ ψ) (bd_not ((bd_not φ) ⊓ (bd_not ψ))) :=
+λ M ne str v xs hM, by simp
+
+lemma inf_semantically_equivalent_not_sup_not {T : L.Theory} {φ ψ : L.bounded_formula α n} :
+  T.semantically_equivalent (φ ⊓ ψ) (bd_not ((bd_not φ) ⊔ (bd_not ψ))) :=
+λ M ne str v xs hM, begin
+  simp only [realize_bounded_formula, has_inf_inf, has_sup_sup, realize_not, not_forall, not_not,
+    exists_prop, and_imp, not_and, and_self],
+  exact λ h1 h2, ⟨h1, h2⟩,
+end
+
+end Theory
+
 end language
 end first_order