models_sentence_iff — Mathlib

English

Let L be a language and T a theory in L, and φ a sentence of L. Then φ is true in every model of T if and only if T entails φ in the bounded sense; equivalently, φ holds in all models M that satisfy T.

Русский

Пусть L — язык, T — теория в L, φ — предложение на языке L. Тогда φ истинно во всех моделях T тогда и только тогда, когда T выводимо (в ограниченном виде) φ; эквивалентно, φ выполняется во всех моделях M, удовлетворяющих T.

LaTeX

$$$T \models^{\mathrm{b}} \varphi \;\Longleftrightarrow\; \forall M : \text{ModelType}(T), M \models \varphi$$$

Lean4

theorem models_sentence_iff {φ : L.Sentence} : T ⊨ᵇ φ ↔ ∀ M : ModelType.{u, v, max u v} T, M ⊨ φ :=
  models_formula_iff.trans (forall_congr' fun _ => Unique.forall_iff)

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