# mathlib3documentation

model_theory.definability

# Definable Sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines what it means for a set over a first-order structure to be definable.

## Main Definitions #

• set.definable is defined so that A.definable L s indicates that the set s of a finite cartesian power of M is definable with parameters in A.
• set.definable₁ is defined so that A.definable₁ L s indicates that (s : set M) is definable with parameters in A.
• set.definable₂ is defined so that A.definable₂ L s indicates that (s : set (M × M)) is definable with parameters in A.
• A first_order.language.definable_set is defined so that L.definable_set A α is the boolean algebra of subsets of α → M defined by formulas with parameters in A.

## Main Results #

• L.definable_set A α forms a boolean_algebra
• set.definable.image_comp shows that definability is closed under projections in finite dimensions.
def set.definable {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] {α : Type u_1} (s : set M)) :
Prop

A subset of a finite Cartesian product of a structure is definable over a set A when membership in the set is given by a first-order formula with parameters from A.

Equations
theorem set.definable.map_expansion {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set M)} {L' : first_order.language} [L'.Structure M] (h : A.definable L s) (φ : L →ᴸ L') [φ.is_expansion_on M] :
A.definable L' s
theorem set.empty_definable_iff {M : Type w} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set M)} :
s (φ : L.formula α), s =
theorem set.definable_iff_empty_definable_with_params {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set M)} :
theorem set.definable.mono {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {B : set M} {s : set M)} (hAs : A.definable L s) (hAB : A B) :
B.definable L s
@[simp]
theorem set.definable_empty {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} :
@[simp]
theorem set.definable_univ {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} :
@[simp]
theorem set.definable.inter {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {f g : set M)} (hf : A.definable L f) (hg : A.definable L g) :
A.definable L (f g)
@[simp]
theorem set.definable.union {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {f g : set M)} (hf : A.definable L f) (hg : A.definable L g) :
A.definable L (f g)
theorem set.definable_finset_inf {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι set M)} (hf : (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L (s.inf f)
theorem set.definable_finset_sup {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι set M)} (hf : (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L (s.sup f)
theorem set.definable_finset_bInter {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι set M)} (hf : (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L ( (i : ι) (H : i s), f i)
theorem set.definable_finset_bUnion {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι set M)} (hf : (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L ( (i : ι) (H : i s), f i)
@[simp]
theorem set.definable.compl {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set M)} (hf : A.definable L s) :
@[simp]
theorem set.definable.sdiff {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s t : set M)} (hs : A.definable L s) (ht : A.definable L t) :
A.definable L (s \ t)
theorem set.definable.preimage_comp {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} (f : α β) {s : set M)} (h : A.definable L s) :
A.definable L ((λ (g : β M), g f) ⁻¹' s)
theorem set.definable.image_comp_equiv {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set M)} (h : A.definable L s) (f : α β) :
A.definable L ((λ (g : β M), g f) '' s)
theorem set.definable.image_comp_sum_inl_fin {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} (m : ) {s : set fin m M)} (h : A.definable L s) :
A.definable L ((λ (g : α fin m M), g sum.inl) '' s)

This lemma is only intended as a helper for definable.image_comp.

theorem set.definable.image_comp_embedding {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set M)} (h : A.definable L s) (f : α β) [finite β] :
A.definable L ((λ (g : β M), g f) '' s)

Shows that definability is closed under finite projections.

theorem set.definable.image_comp {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set M)} (h : A.definable L s) (f : α β) [finite α] [finite β] :
A.definable L ((λ (g : β M), g f) '' s)

Shows that definability is closed under finite projections.

def set.definable₁ {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] (s : set M) :
Prop

A 1-dimensional version of definable, for set M.

Equations
def set.definable₂ {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] (s : set (M × M)) :
Prop

A 2-dimensional version of definable, for set (M × M).

Equations
def first_order.language.definable_set (L : first_order.language) {M : Type w} [L.Structure M] (A : set M) (α : Type u_1) :
Type (max u_1 w)

Definable sets are subsets of finite Cartesian products of a structure such that membership is given by a first-order formula.

Equations
Instances for first_order.language.definable_set`
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem first_order.language.definable_set.le_iff {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : α} :
s t s t
@[simp]
theorem first_order.language.definable_set.mem_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {x : α M} :
@[simp]
theorem first_order.language.definable_set.not_mem_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {x : α M} :
@[simp]
theorem first_order.language.definable_set.mem_sup {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : α} {x : α M} :
x s t x s x t
@[simp]
theorem first_order.language.definable_set.mem_inf {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : α} {x : α M} :
x s t x s x t
@[simp]
theorem first_order.language.definable_set.mem_compl {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s : α} {x : α M} :
x s x s
@[simp]
theorem first_order.language.definable_set.mem_sdiff {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : α} {x : α M} :
x s \ t x s x t
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_sup {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} (s t : α) :
(s t) = s t
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_inf {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} (s t : α) :
(s t) = s t
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_compl {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} (s : α) :
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_sdiff {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} (s t : α) :
(s \ t) = s \ t
@[protected, instance]
Equations