Model theory

ClassFirst-order structure#

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.

FirstOrder.Language.Structure.{u, v, w} (L : FirstOrder.Language) (M : Type w) :
  Type (max (max u v) w)
Sources
MathlibFirstOrder.Language.Structure
Uses 1 · Used by 5
Statement usesNatural number
Used byDefinable set · Elementary embedding · Satisfiability · Substructure · Łoś' theorem

AbbreviationFirst-order formula#

Formula α is the type of formulas with free variables indexed by α and no bound variables in scope.

FirstOrder.Language.Formula.{u, v, u'} (L : FirstOrder.Language) (α : Type u') : Type (max u v u')
Sources
MathlibFirstOrder.Language.Formula
Uses 1 · Used by 4
Statement usesNatural number
Used byDefinable set · Elementary embedding · Satisfiability · Łoś' theorem

DefinitionSatisfiability#

A theory is satisfiable if a structure models it.

FirstOrder.Language.Theory.IsSatisfiable.{u, v} {L : FirstOrder.Language} (T : L.Theory) : Prop
Sources
MathlibFirstOrder.Language.Theory.IsSatisfiable
Uses 2 · Used by 2
Statement usesFirst-order formula · First-order structure
Used byCompactness theorem · Ax–Grothendieck theorem

StructureSubstructure#

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

FirstOrder.Language.Substructure.{u, v, w} (L : FirstOrder.Language) (M : Type w) [L.Structure M] :
  Type w
Sources
MathlibFirstOrder.Language.Substructure
Uses 1 · Used by 1
Statement usesFirst-order structure
Used byLöwenheim-Skolem

DefinitionDefinable set#

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.

Set.Definable.{u, v, w, u₁} {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M]
  {α : Type u₁} (s : Set (α → M)) : Prop
Sources
MathlibSet.Definable
Uses 2 · Used by 1
Statement usesFirst-order formula · First-order structure
Used byAx–Grothendieck theorem

StructureElementary embedding#

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

FirstOrder.Language.ElementaryEmbedding.{u_1, u_2, u_5, u_6} (L : FirstOrder.Language)
  (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] : Type (max u_1 u_2)
Sources
MathlibFirstOrder.Language.ElementaryEmbedding
Uses 2 · Used by 1
Statement usesFirst-order formula · First-order structure
Used byLöwenheim-Skolem

TheoremCompactness theorem#

The Compactness Theorem of first-order logic: A theory is satisfiable if and only if it is finitely satisfiable.

FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable.{u, v} {L : FirstOrder.Language}
  {T : L.Theory} : T.IsSatisfiable ↔ T.IsFinitelySatisfiable
Sources
MathlibFirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
Uses 3 · Used by 1
Statement usesFinite set · Satisfiability
Proof usesŁoś' theorem
Used byLöwenheim-Skolem

TheoremLöwenheim-Skolem#

The Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then there is an elementary embedding in the appropriate direction between then M and a structure of cardinality κ.

FirstOrder.Language.exists_elementaryEmbedding_card_eq.{u, v, w, w'} (L : FirstOrder.Language)
  (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ)
  (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) :
  ∃ N,
    (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧
      Cardinal.mk ↑N = κ
Sources
MathlibFirstOrder.Language.exists_elementaryEmbedding_card_eq
Uses 5
Statement usesCardinal · Elementary embedding
Proof usesCompactness theorem · Ordinal · Substructure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.