realize_iff_of_model_completeTheory

English

If N is a model of Th_L(M), then for every sentence φ, N ⊨ φ iff M ⊨ φ.

Русский

Если N является моделью Th_L(M), то для каждого высказывания φ выполняется N ⊨ φ тогда и только тогда, когда M ⊨ φ.

LaTeX

$$[N \vDash L.\mathrm{completeTheory}(M)] \Rightarrow (N \vDash \varphi \iff M \vDash \varphi)$$

Lean4

theorem realize_iff_of_model_completeTheory [N ⊨ L.completeTheory M] (φ : L.Sentence) : N ⊨ φ ↔ M ⊨ φ :=
  by
  refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩
  contrapose! h
  rw [← Sentence.realize_not] at *
  exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)

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