mathlib documentation

model_theory.basic

Basics on First-Order Structures #

This file defines first-order languages and structures in the style of the Flypitch project.

Main Definitions #

References #

For the Flypitch project:

structure first_order.language  :
Type (max (u_1+1) (u_2+1))
  • functions : Type ?
  • relations : Type ?

A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.

The empty language has no symbols.

Equations
@[nolint]

The type of constants in a given language.

Equations
@[class]

A language is relational when it has no function symbols.

Instances
@[class]

A language is algebraic when it has no relation symbols.

Instances
@[instance]
@[instance]
@[class]
structure first_order.language.Structure (L : first_order.language) (M : Type u_3) :
Type (max u_1 u_2 u_3)

A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

structure first_order.language.hom (L : first_order.language) (M : Type u_3) (N : Type u_4) [L.Structure M] [L.Structure N] :
Type (max u_3 u_4)

A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

structure first_order.language.embedding (L : first_order.language) (M : Type u_3) (N : Type u_4) [L.Structure M] [L.Structure N] :
Type (max u_3 u_4)

An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

structure first_order.language.equiv (L : first_order.language) (M : Type u_3) (N : Type u_4) [L.Structure M] [L.Structure N] :
Type (max u_3 u_4)

An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

@[simp]
theorem first_order.language.hom.has_coe_to_fun_F {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (_x : L.hom M N) :
has_coe_to_fun.F _x = (M → N)
@[simp]
theorem first_order.language.hom.has_coe_to_fun_coe {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (c : L.hom M N) (ᾰ : M) :
@[instance]
def first_order.language.hom.has_coe_to_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :
Equations
@[simp]
theorem first_order.language.hom.to_fun_eq_coe {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f : L.hom M N} :
@[ext]
theorem first_order.language.hom.ext {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] ⦃f g : L.hom M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.hom.ext_iff {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : L.hom M N} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem first_order.language.hom.map_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.hom.map_const {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.hom M N) (c : L.const) :
φ c = c
@[simp]
theorem first_order.language.hom.map_rel {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : } (r : L.relations n) (x : fin n → M) :
def first_order.language.hom.id (L : first_order.language) (M : Type u_3) [L.Structure M] :
L.hom M M

The identity map from a structure to itself

Equations
@[simp]
theorem first_order.language.hom.id_apply {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :
def first_order.language.hom.comp {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (hnp : L.hom N P) (hmn : L.hom M N) :
L.hom M P

Composition of first-order homomorphisms

Equations
@[simp]
theorem first_order.language.hom.comp_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (g : L.hom N P) (f : L.hom M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.hom.comp_assoc {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] {Q : Type u_6} [L.Structure Q] (f : L.hom M N) (g : L.hom N P) (h : L.hom P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order homomorphisms is associative.

@[instance]
Equations
@[simp]
theorem first_order.language.embedding.has_coe_to_fun_coe {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) (ᾰ : M) :
@[simp]
theorem first_order.language.embedding.has_coe_to_fun_F {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (_x : L.embedding M N) :
has_coe_to_fun.F _x = (M → N)
@[simp]
theorem first_order.language.embedding.map_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.embedding M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.embedding.map_const {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.embedding M N) (c : L.const) :
φ c = c
@[simp]
theorem first_order.language.embedding.map_rel {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.embedding M N) {n : } (r : L.relations n) (x : fin n → M) :
def first_order.language.embedding.to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) :
L.hom M N

A first-order embedding is also a first-order homomorphism.

Equations
@[simp]
theorem first_order.language.embedding.coe_to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f : L.embedding M N} :
@[ext]
theorem first_order.language.embedding.ext {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] ⦃f g : L.embedding M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.embedding.ext_iff {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : L.embedding M N} :
f = g ∀ (x : M), f x = g x
theorem first_order.language.embedding.injective {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) :

The identity embedding from a structure to itself

Equations
def first_order.language.embedding.comp {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :
L.embedding M P

Composition of first-order embeddings

Equations
@[simp]
theorem first_order.language.embedding.comp_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (g : L.embedding N P) (f : L.embedding M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.embedding.comp_assoc {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] {Q : Type u_6} [L.Structure Q] (f : L.embedding M N) (g : L.embedding N P) (h : L.embedding P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order embeddings is associative.

def first_order.language.equiv.symm {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
L.equiv N M

The inverse of a first-order equivalence is a first-order equivalence.

Equations
@[instance]
def first_order.language.equiv.has_coe_to_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :
Equations
@[simp]
theorem first_order.language.equiv.has_coe_to_fun_F {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (_x : L.equiv M N) :
has_coe_to_fun.F _x = (M → N)
@[simp]
theorem first_order.language.equiv.has_coe_to_fun_coe {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) (ᾰ : M) :
@[simp]
theorem first_order.language.equiv.map_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.equiv M N) {n : } (f : L.functions n) (x : fin n → M) :
@[simp]
theorem first_order.language.equiv.map_const {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.equiv M N) (c : L.const) :
φ c = c
@[simp]
theorem first_order.language.equiv.map_rel {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : L.equiv M N) {n : } (r : L.relations n) (x : fin n → M) :
def first_order.language.equiv.to_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
L.embedding M N

A first-order equivalence is also a first-order embedding.

Equations
def first_order.language.equiv.to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
L.hom M N

A first-order equivalence is also a first-order embedding.

Equations
@[simp]
theorem first_order.language.equiv.to_embedding_to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[simp]
theorem first_order.language.equiv.coe_to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f : L.equiv M N} :
@[simp]
theorem first_order.language.equiv.coe_to_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[ext]
theorem first_order.language.equiv.ext {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] ⦃f g : L.equiv M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem first_order.language.equiv.ext_iff {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : L.equiv M N} :
f = g ∀ (x : M), f x = g x
theorem first_order.language.equiv.injective {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
def first_order.language.equiv.refl (L : first_order.language) (M : Type u_3) [L.Structure M] :
L.equiv M M

The identity equivalence from a structure to itself

Equations
def first_order.language.equiv.comp {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (hnp : L.equiv N P) (hmn : L.equiv M N) :
L.equiv M P

Composition of first-order equivalences

Equations
@[simp]
theorem first_order.language.equiv.comp_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] (g : L.equiv N P) (f : L.equiv M N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.equiv.comp_assoc {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {P : Type u_5} [L.Structure P] {Q : Type u_6} [L.Structure Q] (f : L.equiv M N) (g : L.equiv N P) (h : L.equiv P Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of first-order homomorphisms is associative.

def first_order.language.closed_under {L : first_order.language} {M : Type u_3} [L.Structure M] {n : } (f : L.functions n) (s : set M) :
Prop

Indicates that a set in a given structure is a closed under a function symbol.

Equations
theorem first_order.language.closed_under.Inf {L : first_order.language} {M : Type u_3} [L.Structure M] {n : } {f : L.functions n} {S : set (set M)} (hS : ∀ (s : set M), s Sfirst_order.language.closed_under f s) :
structure first_order.language.substructure (L : first_order.language) (M : Type u_3) [L.Structure M] :
Type u_3

A substructure of a structure M is a set closed under application of function symbols.

@[simp]
theorem first_order.language.substructure.mem_carrier {L : first_order.language} {M : Type u_3} [L.Structure M] {s : L.substructure M} {x : M} :
x s.carrier x s
@[ext]
theorem first_order.language.substructure.ext {L : first_order.language} {M : Type u_3} [L.Structure M] {S T : L.substructure M} (h : ∀ (x : M), x S x T) :
S = T

Two substructures are equal if they have the same elements.

def first_order.language.substructure.copy {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) (s : set M) (hs : s = S) :

Copy a substructure replacing carrier with a set that is equal to it.

Equations
@[simp]
theorem first_order.language.substructure.coe_copy {L : first_order.language} {M : Type u_3} [L.Structure M] {S : L.substructure M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
theorem first_order.language.substructure.copy_eq {L : first_order.language} {M : Type u_3} [L.Structure M] {S : L.substructure M} {s : set M} (hs : s = S) :
S.copy s hs = S
theorem first_order.language.substructure.const_mem {L : first_order.language} {M : Type u_3} [L.Structure M] {S : L.substructure M} {c : L.const} :
c S
@[instance]

The substructure M of the structure M.

Equations
@[simp]
theorem first_order.language.substructure.mem_top {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :
@[instance]

The inf of two substructures is their intersection.

Equations
@[simp]
theorem first_order.language.substructure.coe_inf {L : first_order.language} {M : Type u_3} [L.Structure M] (p p' : L.substructure M) :
(p p') = p p'
@[simp]
theorem first_order.language.substructure.mem_inf {L : first_order.language} {M : Type u_3} [L.Structure M] {p p' : L.substructure M} {x : M} :
x p p' x p x p'
@[instance]
Equations
@[simp]
theorem first_order.language.substructure.coe_Inf {L : first_order.language} {M : Type u_3} [L.Structure M] (S : set (L.substructure M)) :
(Inf S) = ⋂ (s : L.substructure M) (H : s S), s
theorem first_order.language.substructure.mem_Inf {L : first_order.language} {M : Type u_3} [L.Structure M] {S : set (L.substructure M)} {x : M} :
x Inf S ∀ (p : L.substructure M), p Sx p
theorem first_order.language.substructure.mem_infi {L : first_order.language} {M : Type u_3} [L.Structure M] {ι : Sort u_4} {S : ι → L.substructure M} {x : M} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
@[simp]
theorem first_order.language.substructure.coe_infi {L : first_order.language} {M : Type u_3} [L.Structure M] {ι : Sort u_4} {S : ι → L.substructure M} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
@[instance]

Substructures of a structure form a complete lattice.

Equations

The L.substructure generated by a set.

Equations
@[simp]

The substructure generated by a set includes the set.

@[simp]

A substructure S includes closure L s if and only if it includes s.

Substructure closure of a set is monotone in its argument: if s ⊆ t, then closure L s ≤ closure L t.

theorem first_order.language.substructure.closure_induction {L : first_order.language} {M : Type u_3} [L.Structure M] {s : set M} {p : M → Prop} {x : M} (h : x (first_order.language.substructure.closure L) s) (Hs : ∀ (x : M), x sp x) (Hfun : ∀ {n : } (f : L.functions n), first_order.language.closed_under f (set_of p)) :
p x

An induction principle for closure membership. If p holds for all elements of s, and is preserved under function symbols, then p holds for all elements of the closure of s.

theorem first_order.language.substructure.dense_induction {L : first_order.language} {M : Type u_3} [L.Structure M] {p : M → Prop} (x : M) {s : set M} (hs : (first_order.language.substructure.closure L) s = ) (Hs : ∀ (x : M), x sp x) (Hfun : ∀ {n : } (f : L.functions n), first_order.language.closed_under f (set_of p)) :
p x

If s is a dense set in a structure M, substructure.closure L s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p is preserved under function symbols.

@[simp]

Closure of a substructure S equals S.

theorem first_order.language.substructure.closure_Union {L : first_order.language} {M : Type u_3} [L.Structure M] {ι : Sort u_4} (s : ι → set M) :
def first_order.language.hom.eq_locus {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f g : L.hom M N) :

The substructure of elements x : M such that f x = g x

Equations
theorem first_order.language.hom.eq_on_closure {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : L.hom M N} {s : set M} (h : set.eq_on f g s) :

If two L.homs are equal on a set, then they are equal on its substructure closure.

theorem first_order.language.hom.eq_of_eq_on_top {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : L.hom M N} (h : set.eq_on f g ) :
f = g
theorem first_order.language.hom.eq_of_eq_on_dense {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {s : set M} (hs : (first_order.language.substructure.closure L) s = ) {f g : L.hom M N} (h : set.eq_on f g s) :
f = g