L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (M : ModelType T), ↑M ⊨ φ) ↔ ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ T ⊨ᵇ φ ↔ ¬IsSatisfiable (T ∪ {Formula.not φ})
rw [models_sentence_iff, IsSatisfiable]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
M : ModelType T
⊢ ↑M ⊨ φ
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (M : ModelType T), ↑M ⊨ φ) ↔ ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
refine'
  ⟨fun h1 h2 =>
    (Sentence.realize_not _).1
      (realize_sentence_of_mem (T ∪ {Formula.not φ})
        (Set.subset_union_right _ _ (Set.mem_singleton _)))
      (h1 (h2.some.subtheoryModel (Set.subset_union_left _ _))),
    fun h M => _⟩
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ¬↑M ⊨ φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
M : ModelType T
⊢ ↑M ⊨ φ
contrapose! h
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ¬↑M ⊨ φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
rw [← Sentence.realize_not] at h
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
refine'
  ⟨{  Carrier := M
      is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => _⟩ }⟩
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ
rw [Set.mem_singleton_iff.1 h']
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
exact h