Theorem: LO.Modal.Standard.Theory.unprovable_either (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
⊢ ¬(T *⊢[L]! p ∧ T *⊢[L]! ~p)
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
⊢ False
Tactic:
have ⟨hC₁, hC₂⟩ := hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
⊢ False
Tactic:
have : T *⊢[L]! ⊥ := hC₂ ⨀ hC₁
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this : T *⊢[L]! ⊥
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this : T *⊢[L]! ⊥
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp this
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
⊢ False
Tactic:
have : L ⊬! List.conj' Γ ⟶ ⊥ := consisT hΓ₁
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this✝ : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this : L ⊬! Γ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this✝ : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this : L ⊬! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! List.conj' Γ ⟶ ⊥ := implyLeft_conj_eq_conj'!.mp $ FiniteContext.toₛ! hΓ₂
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this✝¹ : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this✝ : L ⊬! Γ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this✝¹ : T *⊢[L]! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this✝ : L ⊬! Γ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
State after:
no goals