internlm/Lean-Github huggingface dataset:
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 α
⊢ ¬T *⊬[L]! p → ¬(L)-Consistent insert (~p) T
Tactic:
simp [not_not]
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ { ctx := T } ⊢! p → ¬(L)-Consistent insert (p ⟶ ⊥) T
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 α
⊢ { ctx := T } ⊢! p → ¬(L)-Consistent insert (p ⟶ ⊥) T
Tactic:
apply provable_iff_insert_neg_not_Lconsistent.mp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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.neg_provable_iff_insert_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;
  . assumption;
  . apply andImplyIffImplyImply'!.mpr;
    apply imp_swap'!;
    exact FiniteContext.toDef'! hΓ₂;
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.neg_provable_iff_insert_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_swap'! $ andImplyIffImplyImply'!.mp hΓ₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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:
. assumption;
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.neg_provable_iff_insert_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 FiniteContext.toDef'! hΓ₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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 FiniteContext.toDef'! hΓ₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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.neg_provable_iff_insert_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_swap'! $ andImplyIffImplyImply'!.mp hΓ₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_provable_iff_insert_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.neg_provable_iff_insert_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_swap'! $ andImplyIffImplyImply'!.mp hΓ₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_unprovable_iff_insert_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.neg_unprovable_iff_insert_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 neg_provable_iff_insert_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.neg_unprovable_iff_insert_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 neg_provable_iff_insert_not_Lconsistent.mp;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_unprovable_iff_insert_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.neg_unprovable_iff_insert_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.neg_unprovable_iff_insert_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 neg_provable_iff_insert_not_Lconsistent.mpr
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.neg_unprovable_iff_insert_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
Theorem: LO.Modal.Standard.Theory.neg_unprovable_iff_insert_ParametricConsistent
Proof state before:
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
Tactic:
simp [not_not]
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ { ctx := T } ⊢! p ⟶ ⊥ → ¬(L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.neg_unprovable_iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ { ctx := T } ⊢! p ⟶ ⊥ → ¬(L)-Consistent insert p T
Tactic:
apply neg_provable_iff_insert_not_Lconsistent.mp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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₁
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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Γ₁
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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Γ₂
Proof 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
Theorem: LO.Modal.Standard.Theory.unprovable_either
Proof 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
Proof state after:
no goals