internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Theory.not_provable_falsum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
⊢ T *⊬[L]! ⊥
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
hC : { ctx := T } ⊢! ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_provable_falsum
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : { ctx := T } ⊢! ⊥
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp $ hC
Proof state after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : { ctx := T } ⊢! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_provable_falsum
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : { ctx := T } ⊢! ⊥
Γ : 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
hC : { ctx := T } ⊢! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this : L ⊬! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_provable_falsum
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : { ctx := T } ⊢! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this : L ⊬! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! List.conj' Γ ⟶ ⊥ := implyLeft_conj_eq_conj'!.mp 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
hC : { ctx := T } ⊢! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this✝ : L ⊬! Γ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_provable_falsum
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : { ctx := T } ⊢! ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ T
hΓ₂ : Γ ⊢[L]! ⊥
this✝ : L ⊬! Γ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
⊢ ⊥ ∉ T
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
hC : ⊥ ∈ T
⊢ False
Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
⊢ False
Tactic:
have : L ⊬! ⊥ ⟶ ⊥ := consisT (Γ := [⊥]) (by simpa)
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this : L ⊬! ⊥ ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this : L ⊬! ⊥ ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! ⊥ ⟶ ⊥ := efq!
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this✝ : L ⊬! ⊥ ⟶ ⊥
this : L ⊢! ⊥ ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this✝ : L ⊬! ⊥ ⟶ ⊥
this : L ⊢! ⊥ ⟶ ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
⊢ ∀ p ∈ [⊥], p ∈ T
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
⊢ (L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T
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 : ¬((L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T)
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬((L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T)
⊢ False
Tactic:
push_neg at 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 : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := iff_insert_notParametricConsistent.mp hC.1
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 : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
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 : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
obtain ⟨Δ, hΔ₁, hΔ₂⟩ := iff_insert_notParametricConsistent.mp hC.2
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΓ₂ := NegationEquiv.neg_equiv'!.mp hΓ₂
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΔ₂ := NegationEquiv.neg_equiv'!.mp hΔ₂
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥ := demorgan₁'! $ disj₃'! (imp_trans! (implyOfNotOr'! $ demorgan₄'! hΓ₂) disj₁!) (imp_trans! (implyOfNotOr'! $ demorgan₄'! hΔ₂) disj₂!) lem!
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
have := @consisT (Γ ++ Δ) (by
  intro q hq;
  simp at hq;
  rcases hq with hΓ | hΔ
  . exact hΓ₁ _ hΓ;
  . exact hΔ₁ _ hΔ;
)
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥ := unprovable_imp_trans! imply_left_concat_conj'! (consisT (by
  simp;
  intro q hq;
  rcases hq with hΓ | hΔ
  . exact hΓ₁ _ hΓ;
  . exact hΔ₁ _ hΔ;
))
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝¹ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
this : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝¹ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
this : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ ++ Δ, p ∈ T
Tactic:
intro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ++ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ++ Δ
⊢ q ∈ T
Tactic:
simp at hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Tactic:
rcases hq with hΓ | hΔ
Proof state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΓ₁ _ hΓ;
Proof state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΔ₁ _ hΔ;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ₁ _ hΓ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
exact hΔ₁ _ hΔ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ p ∈ Γ ++ Δ, p ∈ T
Tactic:
simp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ (p : Formula α), p ∈ Γ ∨ p ∈ Δ → p ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ (p : Formula α), p ∈ Γ ∨ p ∈ Δ → p ∈ T
Tactic:
intro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.either_consistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Tactic:
rcases hq with hΓ | hΔ
Proof state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T