mathlib documentation

model_theory.bundled

Bundled First-Order Structures #

This file bundles types together with their first-order structure.

Main Definitions #

TODO #

def equiv.bundled_induced (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :

A type bundled with the structure induced by an equivalence.

Equations
@[simp]
theorem equiv.bundled_induced_str (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
@[simp]
theorem equiv.bundled_induced_α (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :
@[simp]
def equiv.bundled_induced_equiv (L : first_order.language) {M : Type w} [L.Structure M] {N : Type w'} (g : M N) :

An equivalence of types as a first-order equivalence to the bundled structure on the codomain.

Equations
@[protected, instance]

The equivalence relation on bundled L.Structures indicating that they are isomorphic.

Equations
structure first_order.language.Theory.Model {L : first_order.language} (T : L.Theory) :
Type (max u v (w+1))

The type of nonempty models of a first-order theory.

Instances for first_order.language.Theory.Model
def first_order.language.Theory.Model.of {L : first_order.language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [nonempty M] :

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

Equations
Instances for first_order.language.Theory.Model.of
@[protected, instance]
def first_order.language.Theory.Model.equiv_induced {L : first_order.language} {T : L.Theory} {M : T.Model} {N : Type w'} (e : M N) :

Maps a bundled model along a bijection.

Equations
@[protected, instance]
noncomputable def first_order.language.Theory.Model.shrink {L : first_order.language} {T : L.Theory} (M : T.Model) [small M] :

Shrinks a small model to a particular universe.

Equations

The reduct of any model of φ.on_Theory T is a model of T.

Equations
noncomputable def first_order.language.Theory.Model.default_expansion {L : first_order.language} {T : L.Theory} {L' : first_order.language} {φ : L →ᴸ L'} (h : φ.injective) [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), φ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), φ.on_relation r))] (M : T.Model) [inhabited M] :

When φ is injective, default_expansion expands a model of T to a model of φ.on_Theory T arbitrarily.

Equations

A model of a theory is also a model of any subtheory.

Equations
Instances for first_order.language.Theory.Model.subtheory_Model
@[protected, instance]
def first_order.language.Theory.model.bundled {L : first_order.language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : nonempty M] (h : M T) :

Bundles M ⊨ T as a T.Model.

Equations
@[simp]
theorem first_order.language.Theory.coe_of {L : first_order.language} {T : L.Theory} {M : Type w} [L.Structure M] [nonempty M] (h : M T) :

A structure that is elementarily equivalent to a model, bundled as a model.

Equations

An elementary substructure of a bundled model as a bundled model.

Equations
Instances for first_order.language.elementary_substructure.to_Model