internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
h : q = p
⊢ q ∈ T
Tactic:
simpa [h] using List.mem_remove_iff.mp hq
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
h : q ∈ T
⊢ q ∈ T
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T ↔ ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Tactic:
. contrapose; push_neg; apply iff_insert_ParametricConsistent.mpr;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Tactic:
. contrapose; push_neg; apply iff_insert_ParametricConsistent.mp;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (¬∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬¬(L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (¬∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬¬(L)-Consistent insert p T
Tactic:
push_neg
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
apply iff_insert_ParametricConsistent.mpr
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Tactic:
contrapose
Proof 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 → ¬∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof 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 → ¬∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
push_neg
Proof 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 → ∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.iff_insert_notParametricConsistent
Proof 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 → ∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
apply iff_insert_ParametricConsistent.mp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!;
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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 Γ
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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Γ₁;
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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Γ₁
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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'!
Proof 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 ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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 Γ
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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Γ₁;
Proof 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
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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Γ₁
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.provable_iff_insert_neg_not_Lconsistent
Proof 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!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof 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:
. contrapose; simp [not_not]; apply provable_iff_insert_neg_not_Lconsistent.mpr;
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof 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:
. contrapose; simp [not_not]; apply provable_iff_insert_neg_not_Lconsistent.mp;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof 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:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert (~p) T → ¬T *⊬[L]! p
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof state before:
case mp
α : 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:
simp [not_not]
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert (p ⟶ ⊥) T → { ctx := T } ⊢! p
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert (p ⟶ ⊥) T → { ctx := T } ⊢! p
Tactic:
apply provable_iff_insert_neg_not_Lconsistent.mpr
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.unprovable_iff_insert_neg_ParametricConsistent
Proof 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:
contrapose
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬T *⊬[L]! p → ¬(L)-Consistent insert (~p) T