# mathlibdocumentation

model_theory.semantics

# Basics on First-Order Semantics #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.realize` is defined so that `t.realize v` is the term `t` evaluated at variables `v`.
• `first_order.language.bounded_formula.realize` is defined so that `φ.realize v xs` is the bounded formula `φ` evaluated at tuples of variables `v` and `xs`.
• `first_order.language.formula.realize` is defined so that `φ.realize v` is the formula `φ` evaluated at variables `v`.
• `first_order.language.sentence.realize` is defined so that `φ.realize M` is the sentence `φ` evaluated in the structure `M`. Also denoted `M ⊨ φ`.
• `first_order.language.Theory.model` is defined so that `T.model M` is true if and only if every sentence of `T` is realized in `M`. Also denoted `T ⊨ φ`.

## Main Results #

• `first_order.language.bounded_formula.realize_to_prenex` shows 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 α n` is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some indexed by `fin n`, which can. For any `φ : L.bounded_formula α (n + 1)`, we define the formula `∀' φ : L.bounded_formula α n` by universally quantifying over the variable indexed by `n : 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
• = (λ (i : fin a_2), (ts i))
@[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 (λ (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} :
= 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 (λ (a : α), (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} :
@[simp]
theorem first_order.language.term.realize_constants_to_vars {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [ M] {t : (L.with_constants α).term β} {v : β M} :
@[simp]
theorem first_order.language.term.realize_vars_to_constants {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [ M] {t : L.term β)} {v : β M} :
theorem first_order.language.term.realize_constants_vars_equiv_left {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [ M] {n : } {t : (L.with_constants α).term fin n)} {v : β M} {xs : fin n M} :
@[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} :
@[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) :
@[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) :
def first_order.language.bounded_formula.realize {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : } (f : 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
@[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} {v : α M} {xs : fin l M} :
φ.not.realize v xs ¬φ.realize v xs
@[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 =
@[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} {v : α M} {xs : fin l M} :
ψ).realize v xs φ.realize v xs ψ.realize v xs
@[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) :
v xs (φ : 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} {v : α M} {xs : fin l M} :
(φ.imp ψ).realize v xs φ.realize v xs ψ.realize v xs
@[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 (λ (i : fin k), (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)} :
@[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
@[simp]
theorem first_order.language.bounded_formula.realize_sup {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : l} {v : α M} {xs : fin l M} :
ψ).realize v xs φ.realize v xs ψ.realize v xs
@[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) :
v xs (φ : 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.succ} {v : α M} {xs : fin l M} :
θ.all.realize v xs (a : M), θ.realize v (fin.snoc xs a)
@[simp]
theorem first_order.language.bounded_formula.realize_ex {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {θ : l.succ} {v : α M} {xs : fin l M} :
θ.ex.realize v xs (a : M), θ.realize v (fin.snoc xs a)
@[simp]
theorem first_order.language.bounded_formula.realize_iff {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : l} {v : α M} {xs : fin l M} :
(φ.iff ψ).realize v xs (φ.realize v xs ψ.realize v xs)
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} {φ : m} {v : α M} {xs : fin n M} :
φ.realize v (xs (fin.cast h))
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 : } {φ : n} {v : α M} {v' : β M} {xs : fin n M} (h1 : (n : ) (t : L.term fin n)) (xs : fin n M), (ft n t) = ) (h2 : (n : ) (R : L.relations n) (x : fin n M), ) :
(λ (_x : ), id) φ).realize v' xs φ.realize v xs
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 : } {φ : 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), (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), ) (hv : (n : ) (xs : fin (k + n) M) (x : M), v (fin.snoc xs x) = v xs) :
φ).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 : } {φ : n} {g : α β fin m} {v : β M} {xs : fin (m + n) 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 : } {φ : n} {v : α M} {xs : fin (n + n') M} (hmn : m + n' n + 1) :
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 : } {φ : n} {v : α M} {xs : fin (n + 1) M} (hmn : m n) :
xs φ.realize v (xs λ (i : fin n), ite (i < m) i.succ)
@[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 : } {φ : n} {v : α M} {xs : fin (n + 1) M} :
theorem first_order.language.bounded_formula.realize_subst {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : } {φ : n} {tf : α L.term β} {v : β M} {xs : fin n M} :
(φ.subst tf).realize v xs φ.realize (λ (a : α), (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 : } {φ : n} {s : set α} (h : (φ.free_var_finset) s) {v : α M} {xs : fin n M} :
theorem first_order.language.bounded_formula.realize_constants_vars_equiv {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [ M] {n : } {φ : β n} {v : β M} {xs : fin n M} :
(sum.elim (λ (a : α), (L.con a)) v) xs φ.realize v xs
@[simp]
theorem first_order.language.bounded_formula.realize_relabel_equiv {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {g : α β} {k : } {φ : k} {v : β M} {xs : fin k M} :
φ.realize (v g) 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 : } {φ : n} {v : α M} {xs : fin n M} :
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] {φ ψ : 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] {φ ψ : 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] (φ : n) {v : α M} {xs : fin n M} :
φ.to_prenex.realize v xs φ.realize v xs
@[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 : } (ψ : 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_inf {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α M} :
ψ).realize v φ.realize v ψ.realize v
@[simp]
theorem first_order.language.formula.realize_imp {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α M} :
(φ.imp ψ).realize v φ.realize v ψ.realize v
@[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 (λ (i : fin k), (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 α} :
@[simp]
theorem first_order.language.formula.realize_sup {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α M} :
ψ).realize v φ.realize v ψ.realize v
@[simp]
theorem first_order.language.formula.realize_iff {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α M} :
(φ.iff ψ).realize v (φ.realize v ψ.realize v)
@[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} :
φ.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
@[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]

A sentence can be evaluated as true or false in a structure.

Equations
@[simp]
theorem first_order.language.formula.realize_equiv_sentence_symm_con {L : first_order.language} (M : Type w) [L.Structure M] {α : Type u'} [(L.with_constants α).Structure M] [ M] (φ : (L.with_constants α).sentence) :
(λ (a : α), (L.con a)) M φ
@[simp]
theorem first_order.language.formula.realize_equiv_sentence {L : first_order.language} (M : Type w) [L.Structure M] {α : Type u'} [(L.with_constants α).Structure M] [ M] (φ : L.formula α) :
φ.realize (λ (a : α), (L.con a))
@[simp]

The complete theory of a structure `M` is the set of all sentences `M` satisfies.

Equations
Instances for `first_order.language.complete_theory`

Two structures are elementarily equivalent when they satisfy the same sentences.

Equations
@[simp]
@[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
@[simp]
theorem first_order.language.Theory.model_iff {L : first_order.language} {M : Type w} [L.Structure M] (T : L.Theory) :
M T (φ : L.sentence), φ T M φ
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]
@[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') :
M T T'
@[simp]
theorem first_order.language.Theory.model_union_iff {L : first_order.language} {M : Type w} [L.Structure M] {T T' : L.Theory} :
M T T' M T M T'
@[protected, instance]
@[simp]
theorem first_order.language.bounded_formula.realize_alls {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : } {φ : n} {v : α M} :
φ.alls.realize v (xs : fin n M), φ.realize v xs
@[simp]
theorem first_order.language.bounded_formula.realize_exs {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : } {φ : n} {v : α M} :
φ.exs.realize v (xs : fin n M), φ.realize v xs
@[simp]
theorem first_order.language.bounded_formula.realize_to_formula {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : } (φ : 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) (φ : n) {v : α M} {xs : fin n M} :
φ.realize (g v) (g xs) φ.realize v xs
@[simp]
theorem first_order.language.equiv.realize_formula {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} (g : L.equiv M N) (φ : L.formula α) {v : α M} :
φ.realize (g v) φ.realize v
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) :
M φ N φ
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_total {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M r.total total (λ (x y : M),
@[protected, instance]
@[protected, instance]
theorem first_order.language.model_distinct_constants_theory (L : first_order.language) {α : Type u'} {M : Type w} [(L.with_constants α).Structure M] (s : set α) :
set.inj_on (λ (i : α), (L.con i)) s
@[symm]
@[trans]
theorem first_order.language.elementarily_equivalent.trans {L : first_order.language} {M : Type w} {N : Type u_3} {P : Type u_4} [L.Structure M] [L.Structure N] [L.Structure P] (MN : N) (NP : P) :
theorem first_order.language.elementarily_equivalent.Theory_model {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {T : L.Theory} [MT : M T] (h : N) :
N T