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

State before:
α : Type u_1
Δ : Sequent α
⊢  ⊢¹ Δ → Semantics.Valid (Valuation α) (List.disj Δ)
Tactic:
intro d v
State after:
α : Type u_1
Δ : Sequent α
d :  ⊢¹ Δ
v : Valuation α
⊢ v ⊧ List.disj Δ

State before:
α : Type u_1
Δ : Sequent α
d :  ⊢¹ Δ
v : Valuation α
⊢ v ⊧ List.disj Δ
Tactic:
induction d
State after:
case axL
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
a✝ : α
⊢ v ⊧ (Formula.atom a✝ :: Formula.natom a✝ :: Δ✝).disj

case verum
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj

case or
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : v ⊧ (p✝ :: q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋎ q✝ :: Δ✝).disj

case and
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋏ q✝ :: Δ✝).disj

case wk
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ Γ✝ : Sequent α
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : v ⊧ List.disj Δ✝
⊢ v ⊧ List.disj Γ✝

case cut
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (~p✝ :: Δ✝).disj
⊢ v ⊧ Δ✝.disj

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v ⊧ (Formula.atom a :: Formula.natom a :: Δ).disj
Tactic:
case axL Δ a =>
  simp[List.map_disj]
  by_cases v a <;> simp[*]
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj
Tactic:
case verum => simp[List.map_disj]
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
d : Derivation (p :: q :: Δ)
ih : v ⊧ (p :: q :: Δ).disj
⊢ v ⊧ (p ⋎ q :: Δ).disj
Tactic:
case or Δ p q d ih =>
  simpa[or_assoc] using ih
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
Tactic:
case wk Δ Γ _ ss ih =>
  have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
  rcases this with ⟨p, hp, hvp⟩
  simp [List.map_disj]; exact ⟨p, ss hp, hvp⟩
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v ⊧ (Formula.atom a :: Formula.natom a :: Δ).disj
Tactic:
simp[List.map_disj]
State after:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v.val a ∨ ¬v.val a ∨ ∃ p ∈ Δ, v ⊧ p

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v.val a ∨ ¬v.val a ∨ ∃ p ∈ Δ, v ⊧ p
Tactic:
by_cases v a <;> simp[*]
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj
Tactic:
simp[List.map_disj]
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
by_cases hv : v ⊧ Δ.disj
State after:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj

case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj

State before:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
simp[hv]
State after:
no goals

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
have : v ⊧ p := by simpa[hv] using ihp
State after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ (p ⋏ q :: Δ).disj

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
have : v ⊧ q := by simpa[hv] using ihq
State after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : v ⊧ q
⊢ v ⊧ (p ⋏ q :: Δ).disj

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : v ⊧ q
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
simp[*]
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ p
Tactic:
simpa[hv] using ihp
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ q
Tactic:
simpa[hv] using ihq
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
d : Derivation (p :: q :: Δ)
ih : v ⊧ (p :: q :: Δ).disj
⊢ v ⊧ (p ⋎ q :: Δ).disj
Tactic:
simpa[or_assoc] using ih
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
Tactic:
have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
State after:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
this : ∃ p ∈ Δ, v ⊧ p
⊢ v ⊧ List.disj Γ

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
this : ∃ p ∈ Δ, v ⊧ p
⊢ v ⊧ List.disj Γ
Tactic:
rcases this with ⟨p, hp, hvp⟩
State after:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ v ⊧ List.disj Γ

State before:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ v ⊧ List.disj Γ
Tactic:
simp [List.map_disj]
State after:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ ∃ p ∈ Γ, v ⊧ p

State before:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ ∃ p ∈ Γ, v ⊧ p
Tactic:
exact ⟨p, ss hp, hvp⟩
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ ∃ p ∈ Δ, v ⊧ p
Tactic:
simpa [List.map_disj] using ih
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
⊢ v ⊧ Δ.disj
Tactic:
by_cases hv : v ⊧ Δ.disj
State after:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ Δ.disj

case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ Δ.disj

State before:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ Δ.disj
Tactic:
simp[hv]
State after:
no goals

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ Δ.disj
Tactic:
have : v ⊧ p := by simpa[hv] using ihp
State after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ Δ.disj

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ Δ.disj
Tactic:
have : ¬v ⊧ p := by simpa[hv] using ihn
State after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ v ⊧ Δ.disj

State before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ v ⊧ Δ.disj
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ p
Tactic:
simpa[hv] using ihp
State after:
no goals

State before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ ¬v ⊧ p
Tactic:
simpa[hv] using ihn
State after:
no goals