isSatisfiable_of_isSatisfiable_onTheory

English

Let φ: L →ᴸ L' be a language morphism. If the theory φ.onTheory(T) is satisfiable, then T is satisfiable.

Русский

Пусть φ: L →ᴸ L'—морфизм языков. Если теория φ.onTheory(T) удовлетворима, то T удовлетворима.

LaTeX

$$$\\forall φ: L \\to_L' L',\\ (φ.onTheory(T) IsSatisfiable) \\rightarrow T.IsSatisfiable$$$

Lean4

theorem isSatisfiable_of_isSatisfiable_onTheory {L' : Language.{w, w'}} (φ : L →ᴸ L')
    (h : (φ.onTheory T).IsSatisfiable) : T.IsSatisfiable :=
  Model.isSatisfiable (h.some.reduct φ)

Похожие утверждения