Theorem: LO.Propositional.Classical.soundness (Logic/Propositional/Classical/Basic/Completeness.lean)

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
⊢ T ⊢! p → T ⊨[Valuation α] p
Tactic:
rintro ⟨Γ, hΓ, d⟩ v hT
State after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
⊢ v ⊧ p

State before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
⊢ v ⊧ p
Tactic:
by_contra hv
State after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ False

State before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ False
Tactic:
have : ∀ v : Valuation α, v ⊧ p ∨ ∃ q ∈ Γ, ¬(v ⊧ q) := by
  simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
State after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ False

State before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Tactic:
have : ∃ q ∈ Γ, ¬v ⊧ q := by simpa [hv] using this v
State after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
this : ∃ q ∈ Γ, ¬v ⊧ q
⊢ False

State before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
this : ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Tactic:
rcases this with ⟨q, hqΓ, hq⟩
State after:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
⊢ False

State before:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
⊢ False
Tactic:
have : v ⊧ q := hT.realize (hΓ q hqΓ)
State after:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
this : v ⊧ q
⊢ False

State before:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
this : v ⊧ q
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
Tactic:
simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ ∃ q ∈ Γ, ¬v ⊧ q
Tactic:
simpa [hv] using this v
State after:
no goals