Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_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;
  . exact hΓ₁;
  . apply andImplyIffImplyImply'!.mpr;
    apply imp_swap'!;
    exact imp_trans! (FiniteContext.toDef'! hΓ₂) dni!;
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_trans! (imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂) dne!;
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:
. exact hΓ₁;
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 imp_trans! (FiniteContext.toDef'! hΓ₂) dni!;
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:
exact hΓ₁
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 imp_trans! (FiniteContext.toDef'! hΓ₂) dni!
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_trans! (imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂) dne!;
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_trans! (imp_swap'! $ andImplyIffImplyImply'!.mp hΓ₂) dne!
State after:
no goals