case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
cases' h.2 φ with hφ hφn
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
simp only [hφ, not_true, iff_false_iff]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ
rw [models_sentence_iff, not_forall]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ Formula.not φ
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ
refine' ⟨h.1.some, _⟩
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ φ
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ Formula.not φ
simp only [Sentence.realize_not, Classical.not_not]
no goals
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ φ
exact models_sentence_iff.1 hφ _
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
simp only [hφn, true_iff_iff]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ
intro hφ
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : ∀ (M : ModelType T), ↑M ⊨ Formula.not φ
hφ : ∀ (M : ModelType T), ↑M ⊨ φ
⊢ False
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False
rw [models_sentence_iff] at *
no goals
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : ∀ (M : ModelType T), ↑M ⊨ Formula.not φ
hφ : ∀ (M : ModelType T), ↑M ⊨ φ
⊢ False
exact hφn h.1.some (hφ _)