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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ T *⊢[L]! ~p ↔ ¬(L)-Consistent insert p T
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ T *⊢[L]! ~p → ¬(L)-Consistent insert p T

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → T *⊢[L]! ~p

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ T *⊢[L]! ~p → ¬(L)-Consistent insert p T

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → T *⊢[L]! ~p
Tactic:
. intro h;
  apply iff_insert_notParametricConsistent.mpr;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h;
  existsi Γ;
  constructor;
  . assumption;
  . apply andImplyIffImplyImply'!.mpr;
    apply imp_swap'!;
    exact FiniteContext.toDef'! hΓ₂;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → T *⊢[L]! ~p

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → T *⊢[L]! ~p
Tactic:
. intro h;
  apply Context.provable_iff.mpr;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := iff_insert_notParametricConsistent.mp h;
  existsi Γ;
  constructor;
  . exact hΓ₁;
  . exact FiniteContext.ofDef'! $ imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ T *⊢[L]! ~p → ¬(L)-Consistent insert p T
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
⊢ ¬(L)-Consistent insert p T

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
⊢ ¬(L)-Consistent insert p T
Tactic:
apply iff_insert_notParametricConsistent.mpr
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
⊢ ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

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

State before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
existsi Γ
State after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

State before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
constructor
State after:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ ∀ p ∈ Γ, p ∈ T

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

State before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ ∀ p ∈ Γ, p ∈ T

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
. assumption;
State after:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

State before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
. apply andImplyIffImplyImply'!.mpr;
  apply imp_swap'!;
  exact FiniteContext.toDef'! hΓ₂;
State after:
no goals

State before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ ∀ p ∈ Γ, p ∈ T
Tactic:
assumption
State after:
no goals

State before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
apply andImplyIffImplyImply'!.mpr
State after:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⟶ Γ.conj' ⟶ ⊥

State before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! p ⟶ Γ.conj' ⟶ ⊥
Tactic:
apply imp_swap'!
State after:
case mp.intro.intro.right.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! Γ.conj' ⟶ p ⟶ ⊥

State before:
case mp.intro.intro.right.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : T *⊢[L]! ~p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ~p
⊢ L ⊢! Γ.conj' ⟶ p ⟶ ⊥
Tactic:
exact FiniteContext.toDef'! hΓ₂
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → T *⊢[L]! ~p
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
⊢ T *⊢[L]! ~p

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
⊢ T *⊢[L]! ~p
Tactic:
apply Context.provable_iff.mpr
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ T) ∧ Δ ⊢[L]! ~p

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ T) ∧ Δ ⊢[L]! ~p
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := iff_insert_notParametricConsistent.mp h
State after:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ T) ∧ Δ ⊢[L]! ~p

State before:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ T) ∧ Δ ⊢[L]! ~p
Tactic:
existsi Γ
State after:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ (∀ q ∈ Γ, q ∈ T) ∧ Γ ⊢[L]! ~p

State before:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ (∀ q ∈ Γ, q ∈ T) ∧ Γ ⊢[L]! ~p
Tactic:
constructor
State after:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ T

case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ Γ ⊢[L]! ~p

State before:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ T

case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ Γ ⊢[L]! ~p
Tactic:
. exact hΓ₁;
State after:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ Γ ⊢[L]! ~p

State before:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ Γ ⊢[L]! ~p
Tactic:
. exact FiniteContext.ofDef'! $ imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂;
State after:
no goals

State before:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ T
Tactic:
exact hΓ₁
State after:
no goals

State before:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ¬(L)-Consistent insert p T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ Γ ⊢[L]! ~p
Tactic:
exact FiniteContext.ofDef'! $ imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂
State after:
no goals