realize_sentence_iff — Mathlib

English

In a complete theory, either φ is realized or its negation is realized in any model.

Русский

В полной теории либо φ реализуется, либо не φ реализуется в любой модели.

LaTeX

$$$M \\models φ \\lor M \\not\\models φ$ in complete theories$$

Lean4

theorem realize_sentence_iff (h : T.IsComplete) (φ : L.Sentence) (M : Type*) [L.Structure M] [M ⊨ T] [Nonempty M] :
    M ⊨ φ ↔ T ⊨ᵇ φ := by
  rcases h.2 φ with hφ | hφn
  · exact iff_of_true (hφ.realize_sentence M) hφ
  · exact iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M)) ((h.models_not_iff φ).1 hφn)

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