Basics on First-Order Semantics #
This file defines the interpretations of first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.
Main Definitions #
first_order.language.term.realizeis defined so thatt.realize vis the termtevaluated at variablesv.first_order.language.bounded_formula.realizeis defined so thatφ.realize v xsis the bounded formulaφevaluated at tuples of variablesvandxs.first_order.language.formula.realizeis defined so thatφ.realize vis the formulaφevaluated at variablesv.first_order.language.sentence.realizeis defined so thatφ.realize Mis the sentenceφevaluated in the structureM. Also denotedM ⊨ φ.first_order.language.Theory.modelis defined so thatT.model Mis true if and only if every sentence ofTis realized inM. Also denotedT ⊨ φ.
Main Results #
first_order.language.bounded_formula.realize_to_prenexshows that the prenex normal form of a formula has the same realization as the original formula.- Several results in this file show that syntactic constructions such as
relabel,cast_le,lift_at,subst, and the actions of language maps commute with realization of terms, formulas, sentences, and theories.
Implementation Notes #
- Formulas use a modified version of de Bruijn variables. Specifically, a
L.bounded_formula α nis a formula with some variables indexed by a typeα, which cannot be quantified over, and some indexed byfin n, which can. For anyφ : L.bounded_formula α (n + 1), we define the formula∀' φ : L.bounded_formula α nby universally quantifying over the variable indexed byn : fin (n + 1).
References #
For the Flypitch project:
@[simp]
def
first_order.language.term.realize
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
(v : α → M)
(t : L.term α) :
M
A term t with variables indexed by α can be evaluated by giving a value to each variable.
Equations
- first_order.language.term.realize v (first_order.language.term.func f ts) = first_order.language.Structure.fun_map f (λ (i : fin a_2), first_order.language.term.realize v (ts i))
- first_order.language.term.realize v (first_order.language.term.var k) = v k
@[simp]
theorem
first_order.language.term.realize_relabel
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{t : L.term α}
{g : α → β}
{v : β → M} :
@[simp]
theorem
first_order.language.term.realize_lift_at
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n n' m : ℕ}
{t : L.term (α ⊕ fin n)}
{v : α ⊕ fin (n + n') → M} :
first_order.language.term.realize v (first_order.language.term.lift_at n' m t) = first_order.language.term.realize (v ∘ sum.map id (λ (i : fin n), ite (↑i < m) (⇑(fin.cast_add n') i) (⇑(fin.add_nat n') i))) t
@[simp]
theorem
first_order.language.term.realize_constants
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{c : L.constants}
{v : α → M} :
@[simp]
theorem
first_order.language.term.realize_functions_apply₁
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{f : L.functions 1}
{t : L.term α}
{v : α → M} :
@[simp]
theorem
first_order.language.term.realize_functions_apply₂
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{f : L.functions 2}
{t₁ t₂ : L.term α}
{v : α → M} :
theorem
first_order.language.term.realize_con
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{A : set M}
{a : ↥A}
{v : α → M} :
first_order.language.term.realize v (L.con a).term = ↑a
@[simp]
theorem
first_order.language.term.realize_subst
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{t : L.term α}
{tf : α → L.term β}
{v : β → M} :
first_order.language.term.realize v (t.subst tf) = first_order.language.term.realize (λ (a : α), first_order.language.term.realize v (tf a)) t
@[simp]
theorem
first_order.language.term.realize_restrict_var
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[decidable_eq α]
{t : L.term α}
{s : set α}
(h : ↑(t.var_finset) ⊆ s)
{v : α → M} :
@[simp]
theorem
first_order.language.term.realize_restrict_var_left
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[decidable_eq α]
{γ : Type u_1}
{t : L.term (α ⊕ γ)}
{s : set α}
(h : ↑(t.var_finset_left) ⊆ s)
{v : α → M}
{xs : γ → M} :
first_order.language.term.realize (sum.elim (v ∘ coe) xs) (t.restrict_var_left (set.inclusion h)) = first_order.language.term.realize (sum.elim v xs) t
@[simp]
theorem
first_order.language.Lhom.realize_on_term
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
(t : L.term α)
(v : α → M) :
@[simp]
theorem
first_order.language.hom.realize_term
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
{α : Type u'}
(g : L.hom M N)
{t : L.term α}
{v : α → M} :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
@[simp]
theorem
first_order.language.embedding.realize_term
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
{α : Type u'}
{v : α → M}
(t : L.term α)
(g : L.embedding M N) :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
@[simp]
theorem
first_order.language.equiv.realize_term
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
{α : Type u'}
{v : α → M}
(t : L.term α)
(g : L.equiv M N) :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
def
first_order.language.bounded_formula.realize
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
(f : L.bounded_formula α l)
(v : α → M)
(xs : fin l → M) :
Prop
A bounded formula can be evaluated as true or false by giving values to each free variable.
Equations
- f.all.realize v xs = ∀ (x : M), f.realize v (fin.snoc xs x)
- (f₁.imp f₂).realize v xs = (f₁.realize v xs → f₂.realize v xs)
- (first_order.language.bounded_formula.rel R ts).realize v xs = first_order.language.Structure.rel_map R (λ (i : fin a_5), first_order.language.term.realize (sum.elim v xs) (ts i))
- (first_order.language.bounded_formula.equal t₁ t₂).realize v xs = (first_order.language.term.realize (sum.elim v xs) t₁ = first_order.language.term.realize (sum.elim v xs) t₂)
- first_order.language.bounded_formula.falsum.realize v xs = false
@[simp]
theorem
first_order.language.bounded_formula.realize_bot
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_not
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{φ : L.bounded_formula α l}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_bd_equal
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M}
(t₁ t₂ : L.term (α ⊕ fin l)) :
(t₁.bd_equal t₂).realize v xs ↔ first_order.language.term.realize (sum.elim v xs) t₁ = first_order.language.term.realize (sum.elim v xs) t₂
@[simp]
theorem
first_order.language.bounded_formula.realize_top
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_inf
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{φ ψ : L.bounded_formula α l}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_foldr_inf
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
(l : list (L.bounded_formula α n))
(v : α → M)
(xs : fin n → M) :
(list.foldr has_inf.inf ⊤ l).realize v xs ↔ ∀ (φ : L.bounded_formula α n), φ ∈ l → φ.realize v xs
@[simp]
theorem
first_order.language.bounded_formula.realize_imp
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{φ ψ : L.bounded_formula α l}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_rel
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M}
{k : ℕ}
{R : L.relations k}
{ts : fin k → L.term (α ⊕ fin l)} :
(R.bounded_formula ts).realize v xs ↔ first_order.language.Structure.rel_map R (λ (i : fin k), first_order.language.term.realize (sum.elim v xs) (ts i))
@[simp]
theorem
first_order.language.bounded_formula.realize_rel₁
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M}
{R : L.relations 1}
{t : L.term (α ⊕ fin l)} :
(R.bounded_formula₁ t).realize v xs ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize (sum.elim v xs) t]
@[simp]
theorem
first_order.language.bounded_formula.realize_rel₂
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{v : α → M}
{xs : fin l → M}
{R : L.relations 2}
{t₁ t₂ : L.term (α ⊕ fin l)} :
(R.bounded_formula₂ t₁ t₂).realize v xs ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize (sum.elim v xs) t₁, first_order.language.term.realize (sum.elim v xs) t₂]
@[simp]
theorem
first_order.language.bounded_formula.realize_sup
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{φ ψ : L.bounded_formula α l}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_foldr_sup
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
(l : list (L.bounded_formula α n))
(v : α → M)
(xs : fin n → M) :
(list.foldr has_sup.sup ⊥ l).realize v xs ↔ ∃ (φ : L.bounded_formula α n) (H : φ ∈ l), φ.realize v xs
@[simp]
theorem
first_order.language.bounded_formula.realize_all
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{θ : L.bounded_formula α l.succ}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_ex
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{θ : L.bounded_formula α l.succ}
{v : α → M}
{xs : fin l → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_iff
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{l : ℕ}
{φ ψ : L.bounded_formula α l}
{v : α → M}
{xs : fin l → M} :
theorem
first_order.language.bounded_formula.realize_cast_le_of_eq
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{m n : ℕ}
(h : m = n)
{h' : m ≤ n}
{φ : L.bounded_formula α m}
{v : α → M}
{xs : fin n → M} :
theorem
first_order.language.bounded_formula.realize_map_term_rel_id
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[L'.Structure M]
{ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin n)}
{fr : Π (n : ℕ), L.relations n → L'.relations n}
{n : ℕ}
{φ : L.bounded_formula α n}
{v : α → M}
{v' : β → M}
{xs : fin n → M}
(h1 : ∀ (n : ℕ) (t : L.term (α ⊕ fin n)) (xs : fin n → M), first_order.language.term.realize (sum.elim v' xs) (ft n t) = first_order.language.term.realize (sum.elim v xs) t)
(h2 : ∀ (n : ℕ) (R : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map (fr n R) x = first_order.language.Structure.rel_map R x) :
theorem
first_order.language.bounded_formula.realize_map_term_rel_add_cast_le
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
[L'.Structure M]
{k : ℕ}
{ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin (k + n))}
{fr : Π (n : ℕ), L.relations n → L'.relations n}
{n : ℕ}
{φ : L.bounded_formula α n}
(v : Π {n : ℕ}, (fin (k + n) → M) → α → M)
{v' : β → M}
(xs : fin (k + n) → M)
(h1 : ∀ (n : ℕ) (t : L.term (α ⊕ fin n)) (xs' : fin (k + n) → M), first_order.language.term.realize (sum.elim v' xs') (ft n t) = first_order.language.term.realize (sum.elim (v xs') (xs' ∘ ⇑(fin.nat_add k))) t)
(h2 : ∀ (n : ℕ) (R : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map (fr n R) x = first_order.language.Structure.rel_map R x)
(hv : ∀ (n : ℕ) (xs : fin (k + n) → M) (x : M), v (fin.snoc xs x) = v xs) :
(first_order.language.bounded_formula.map_term_rel ft fr (λ (n : ℕ), first_order.language.bounded_formula.cast_le _) φ).realize v' xs ↔ φ.realize (v xs) (xs ∘ ⇑(fin.nat_add k))
theorem
first_order.language.bounded_formula.realize_relabel
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{m n : ℕ}
{φ : L.bounded_formula α n}
{g : α → β ⊕ fin m}
{v : β → M}
{xs : fin (m + n) → M} :
(first_order.language.bounded_formula.relabel g φ).realize v xs ↔ φ.realize (sum.elim v (xs ∘ ⇑(fin.cast_add n)) ∘ g) (xs ∘ ⇑(fin.nat_add m))
theorem
first_order.language.bounded_formula.realize_lift_at
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n n' m : ℕ}
{φ : L.bounded_formula α n}
{v : α → M}
{xs : fin (n + n') → M}
(hmn : m + n' ≤ n + 1) :
(first_order.language.bounded_formula.lift_at n' m φ).realize v xs ↔ φ.realize v (xs ∘ λ (i : fin n), ite (↑i < m) (⇑(fin.cast_add n') i) (⇑(fin.add_nat n') i))
theorem
first_order.language.bounded_formula.realize_lift_at_one
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n m : ℕ}
{φ : L.bounded_formula α n}
{v : α → M}
{xs : fin (n + 1) → M}
(hmn : m ≤ n) :
@[simp]
theorem
first_order.language.bounded_formula.realize_lift_at_one_self
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
{φ : L.bounded_formula α n}
{v : α → M}
{xs : fin (n + 1) → M} :
(first_order.language.bounded_formula.lift_at 1 n φ).realize v xs ↔ φ.realize v (xs ∘ ⇑fin.cast_succ)
theorem
first_order.language.bounded_formula.realize_subst
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{n : ℕ}
{φ : L.bounded_formula α n}
{tf : α → L.term β}
{v : β → M}
{xs : fin n → M} :
(φ.subst tf).realize v xs ↔ φ.realize (λ (a : α), first_order.language.term.realize v (tf a)) xs
@[simp]
theorem
first_order.language.bounded_formula.realize_restrict_free_var
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[decidable_eq α]
{n : ℕ}
{φ : L.bounded_formula α n}
{s : set α}
(h : ↑(φ.free_var_finset) ⊆ s)
{v : α → M}
{xs : fin n → M} :
(φ.restrict_free_var (set.inclusion h)).realize (v ∘ coe) xs ↔ φ.realize v xs
theorem
first_order.language.bounded_formula.realize_all_lift_at_one_self
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[nonempty M]
{n : ℕ}
{φ : L.bounded_formula α n}
{v : α → M}
{xs : fin n → M} :
(first_order.language.bounded_formula.lift_at 1 n φ).all.realize v xs ↔ φ.realize v xs
theorem
first_order.language.bounded_formula.realize_to_prenex_imp_right
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
[nonempty M]
{φ ψ : L.bounded_formula α n}
(hφ : φ.is_qf)
(hψ : ψ.is_prenex)
{v : α → M}
{xs : fin n → M} :
(φ.to_prenex_imp_right ψ).realize v xs ↔ (φ.imp ψ).realize v xs
theorem
first_order.language.bounded_formula.realize_to_prenex_imp
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
[nonempty M]
{φ ψ : L.bounded_formula α n}
(hφ : φ.is_prenex)
(hψ : ψ.is_prenex)
{v : α → M}
{xs : fin n → M} :
(φ.to_prenex_imp ψ).realize v xs ↔ (φ.imp ψ).realize v xs
@[simp]
theorem
first_order.language.bounded_formula.realize_to_prenex
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
[nonempty M]
(φ : L.bounded_formula α n)
{v : α → M}
{xs : fin n → M} :
@[simp]
theorem
first_order.language.Lhom.realize_on_bounded_formula
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
{n : ℕ}
(ψ : L.bounded_formula α n)
{v : α → M}
{xs : fin n → M} :
(φ.on_bounded_formula ψ).realize v xs ↔ ψ.realize v xs
def
first_order.language.formula.realize
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
(φ : L.formula α)
(v : α → M) :
Prop
A formula can be evaluated as true or false by giving values to each free variable.
Equations
@[simp]
theorem
first_order.language.formula.realize_not
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{φ : L.formula α}
{v : α → M} :
@[simp]
theorem
first_order.language.formula.realize_bot
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M} :
@[simp]
theorem
first_order.language.formula.realize_top
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M} :
@[simp]
theorem
first_order.language.formula.realize_imp
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{φ ψ : L.formula α}
{v : α → M} :
@[simp]
theorem
first_order.language.formula.realize_rel
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{k : ℕ}
{R : L.relations k}
{ts : fin k → L.term α} :
(R.formula ts).realize v ↔ first_order.language.Structure.rel_map R (λ (i : fin k), first_order.language.term.realize v (ts i))
@[simp]
theorem
first_order.language.formula.realize_rel₁
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{R : L.relations 1}
{t : L.term α} :
@[simp]
theorem
first_order.language.formula.realize_rel₂
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{v : α → M}
{R : L.relations 2}
{t₁ t₂ : L.term α} :
(R.formula₂ t₁ t₂).realize v ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize v t₁, first_order.language.term.realize v t₂]
@[simp]
theorem
first_order.language.formula.realize_relabel
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{β : Type v'}
{φ : L.formula α}
{g : α → β}
{v : β → M} :
(first_order.language.formula.relabel g φ).realize v ↔ φ.realize (v ∘ g)
theorem
first_order.language.formula.realize_relabel_sum_inr
{L : first_order.language}
{M : Type w}
[L.Structure M]
{n : ℕ}
(φ : L.formula (fin n))
{v : empty → M}
{x : fin n → M} :
@[simp]
theorem
first_order.language.formula.realize_equal
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{t₁ t₂ : L.term α}
{x : α → M} :
(t₁.equal t₂).realize x ↔ first_order.language.term.realize x t₁ = first_order.language.term.realize x t₂
@[simp]
theorem
first_order.language.formula.realize_graph
{L : first_order.language}
{M : Type w}
[L.Structure M]
{n : ℕ}
{f : L.functions n}
{x : fin n → M}
{y : M} :
@[simp]
theorem
first_order.language.Lhom.realize_on_formula
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
(ψ : L.formula α)
{v : α → M} :
(φ.on_formula ψ).realize v ↔ ψ.realize v
@[simp]
theorem
first_order.language.Lhom.set_of_realize_on_formula
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
(ψ : L.formula α) :
def
first_order.language.sentence.realize
{L : first_order.language}
(M : Type w)
[L.Structure M]
(φ : L.sentence) :
Prop
A sentence can be evaluated as true or false in a structure.
Equations
@[simp]
theorem
first_order.language.sentence.realize_not
{L : first_order.language}
(M : Type w)
[L.Structure M]
{φ : L.sentence} :
M ⊨ first_order.language.formula.not φ ↔ ¬M ⊨ φ
@[simp]
theorem
first_order.language.Lhom.realize_on_sentence
{L : first_order.language}
{L' : first_order.language}
(M : Type w)
[L.Structure M]
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
(ψ : L.sentence) :
M ⊨ φ.on_sentence ψ ↔ M ⊨ ψ
def
first_order.language.complete_theory
(L : first_order.language)
(M : Type w)
[L.Structure M] :
L.Theory
The complete theory of a structure M is the set of all sentences M satisfies.
Equations
- L.complete_theory M = {φ : L.sentence | M ⊨ φ}
Instances for first_order.language.complete_theory
def
first_order.language.elementarily_equivalent
(L : first_order.language)
(M : Type w)
(N : Type u_3)
[L.Structure M]
[L.Structure N] :
Prop
Two structures are elementarily equivalent when they satisfy the same sentences.
Equations
- L.elementarily_equivalent M N = (L.complete_theory M = L.complete_theory N)
@[simp]
theorem
first_order.language.mem_complete_theory
{L : first_order.language}
{M : Type w}
[L.Structure M]
{φ : L.sentence} :
φ ∈ L.complete_theory M ↔ M ⊨ φ
theorem
first_order.language.elementarily_equivalent_iff
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N] :
@[class]
structure
first_order.language.Theory.model
{L : first_order.language}
(M : Type w)
[L.Structure M]
(T : L.Theory) :
Prop
A model of a theory is a structure in which every sentence is realized as true.
Instances of this typeclass
- first_order.language.model_empty
- first_order.language.model_complete_theory
- first_order.language.model_infinite_theory
- first_order.language.model_nonempty
- first_order.language.elementary_substructure.Theory_model
- first_order.language.Theory.Model.is_model
- first_order.language.simple_graph_model
- first_order.language.model_preorder
- first_order.language.model_partial_order
- first_order.language.model_linear_order
- first_order.language.model_DLO
@[simp]
theorem
first_order.language.Theory.model_iff
{L : first_order.language}
{M : Type w}
[L.Structure M]
(T : L.Theory) :
theorem
first_order.language.Theory.realize_sentence_of_mem
{L : first_order.language}
{M : Type w}
[L.Structure M]
(T : L.Theory)
[M ⊨ T]
{φ : L.sentence}
(h : φ ∈ T) :
M ⊨ φ
@[simp]
theorem
first_order.language.Lhom.on_Theory_model
{L : first_order.language}
{L' : first_order.language}
{M : Type w}
[L.Structure M]
[L'.Structure M]
(φ : L →ᴸ L')
[φ.is_expansion_on M]
(T : L.Theory) :
@[protected, instance]
theorem
first_order.language.Theory.model.mono
{L : first_order.language}
{M : Type w}
[L.Structure M]
{T T' : L.Theory}
(h : M ⊨ T')
(hs : T ⊆ T') :
M ⊨ T
theorem
first_order.language.Theory.model.union
{L : first_order.language}
{M : Type w}
[L.Structure M]
{T T' : L.Theory}
(h : M ⊨ T)
(h' : M ⊨ T') :
theorem
first_order.language.Theory.model_singleton_iff
{L : first_order.language}
{M : Type w}
[L.Structure M]
{φ : L.sentence} :
theorem
first_order.language.Theory.model_iff_subset_complete_theory
{L : first_order.language}
{M : Type w}
[L.Structure M]
{T : L.Theory} :
M ⊨ T ↔ T ⊆ L.complete_theory M
@[protected, instance]
def
first_order.language.model_complete_theory
{L : first_order.language}
{M : Type w}
[L.Structure M] :
M ⊨ L.complete_theory M
theorem
first_order.language.realize_iff_of_model_complete_theory
{L : first_order.language}
(M : Type w)
(N : Type u_3)
[L.Structure M]
[L.Structure N]
[N ⊨ L.complete_theory M]
(φ : L.sentence) :
@[simp]
theorem
first_order.language.bounded_formula.realize_alls
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
{φ : L.bounded_formula α n}
{v : α → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_exs
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
{φ : L.bounded_formula α n}
{v : α → M} :
@[simp]
theorem
first_order.language.bounded_formula.realize_to_formula
{L : first_order.language}
{M : Type w}
[L.Structure M]
{α : Type u'}
{n : ℕ}
(φ : L.bounded_formula α n)
(v : α ⊕ fin n → M) :
@[simp]
theorem
first_order.language.equiv.realize_bounded_formula
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
{α : Type u'}
{n : ℕ}
(g : L.equiv M N)
(φ : L.bounded_formula α n)
{v : α → M}
{xs : fin n → M} :
theorem
first_order.language.equiv.realize_sentence
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
(g : L.equiv M N)
(φ : L.sentence) :
theorem
first_order.language.equiv.Theory_model
{L : first_order.language}
{M : Type w}
{N : Type u_3}
[L.Structure M]
[L.Structure N]
{T : L.Theory}
(g : L.equiv M N)
[M ⊨ T] :
N ⊨ T
@[simp]
theorem
first_order.language.relations.realize_reflexive
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.reflexive ↔ reflexive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.relations.realize_irreflexive
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.irreflexive ↔ irreflexive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.relations.realize_symmetric
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.symmetric ↔ symmetric (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.relations.realize_antisymmetric
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.antisymmetric ↔ anti_symmetric (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.relations.realize_transitive
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.transitive ↔ transitive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.relations.realize_total
{L : first_order.language}
{M : Type w}
[L.Structure M]
{r : L.relations 2} :
M ⊨ r.total ↔ total (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
@[simp]
theorem
first_order.language.sentence.realize_card_ge
(L : first_order.language)
{M : Type w}
[L.Structure M]
(n : ℕ) :
M ⊨ first_order.language.sentence.card_ge L n ↔ ↑n ≤ cardinal.mk M
@[simp]
theorem
first_order.language.model_infinite_theory_iff
(L : first_order.language)
{M : Type w}
[L.Structure M] :
M ⊨ L.infinite_theory ↔ infinite M
@[protected, instance]
def
first_order.language.model_infinite_theory
(L : first_order.language)
{M : Type w}
[L.Structure M]
[h : infinite M] :
M ⊨ L.infinite_theory
@[simp]
theorem
first_order.language.model_nonempty_theory_iff
(L : first_order.language)
{M : Type w}
[L.Structure M] :
M ⊨ L.nonempty_theory ↔ nonempty M
@[protected, instance]
def
first_order.language.model_nonempty
(L : first_order.language)
{M : Type w}
[L.Structure M]
[h : nonempty M] :
M ⊨ L.nonempty_theory
theorem
first_order.language.model_distinct_constants_theory
(L : first_order.language)
{α : Type u'}
{M : Type w}
[(L.with_constants α).Structure M]
(s : set α) :
M ⊨ L.distinct_constants_theory s ↔ set.inj_on (λ (i : α), ↑(L.con i)) s
theorem
first_order.language.card_le_of_model_distinct_constants_theory
(L : first_order.language)
{α : Type u'}
(s : set α)
(M : Type w)
[(L.with_constants α).Structure M]
[h : M ⊨ L.distinct_constants_theory s] :
(cardinal.mk ↥s).lift ≤ (cardinal.mk M).lift