internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mpr.disj₃
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! ~~((p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝)
Tactic:
apply dni'!
Proof state after:
case mpr.disj₃.b
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mpr.disj₃.b
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p ↔ 𝐂𝐥 ⊢! ~p
Tactic:
constructor
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p

case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p

case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
. intro d; exact glivenko.mp $ dni'! d;
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
. intro d; exact tne'! $ glivenko.mpr d;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p
Tactic:
intro d
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~p
⊢ 𝐂𝐥 ⊢! ~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~p
⊢ 𝐂𝐥 ⊢! ~p
Tactic:
exact glivenko.mp $ dni'! d
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
intro d
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! ~p
⊢ 𝐈𝐧𝐭 ⊢! ~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! ~p
⊢ 𝐈𝐧𝐭 ⊢! ~p
Tactic:
exact tne'! $ glivenko.mpr d
Proof state after:
no goals
Theorem: LO.Gentzen.provable_iff
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ 𝓣 ⊢! p → ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
rintro ⟨b⟩
Proof state after:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Theorem: LO.Gentzen.provable_iff
Proof state before:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
rcases proofEquivDerivation b with ⟨Δ, d⟩
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
Δ : { Δ // ∀ π ∈ Δ, π ∈ 𝓣 }
d : ↑Δ ⊢² [p]
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Theorem: LO.Gentzen.provable_iff
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
Δ : { Δ // ∀ π ∈ Δ, π ∈ 𝓣 }
d : ↑Δ ⊢² [p]
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
exact ⟨Δ, Δ.prop, ⟨d⟩⟩
Proof state after:
no goals
Theorem: LO.Gentzen.provable_iff
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ (∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]) → 𝓣 ⊢! p
Tactic:
rintro ⟨Δ, h, ⟨d⟩⟩
Proof state after:
case intro.intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ π ∈ Δ, π ∈ 𝓣
d : Δ ⊢² [p]
⊢ 𝓣 ⊢! p
Theorem: LO.Gentzen.provable_iff
Proof state before:
case intro.intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ π ∈ Δ, π ∈ 𝓣
d : Δ ⊢² [p]
⊢ 𝓣 ⊢! p
Tactic:
exact ⟨proofEquivDerivation.symm ⟨⟨Δ, h⟩, d⟩⟩
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ System.Consistent 𝓣 → IsEmpty (𝓣 ⊢' [])
Tactic:
contrapose
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬IsEmpty (𝓣 ⊢' []) → ¬System.Consistent 𝓣
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬IsEmpty (𝓣 ⊢' []) → ¬System.Consistent 𝓣
Tactic:
simp [System.Consistent, System.not_consistent_iff_inconsistent, System.inconsistent_iff_provable_bot]
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢' [] → 𝓣 ⊢! ⊥
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢' [] → 𝓣 ⊢! ⊥
Tactic:
intro b
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ 𝓣 ⊢! ⊥
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ 𝓣 ⊢! ⊥
Tactic:
exact ⟨b.wk (by simp)⟩
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ [] ⊆ [⊥]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ IsEmpty (𝓣 ⊢' []) → System.Consistent 𝓣
Tactic:
contrapose
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬System.Consistent 𝓣 → ¬IsEmpty (𝓣 ⊢' [])
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬System.Consistent 𝓣 → ¬IsEmpty (𝓣 ⊢' [])
Tactic:
simp [System.Consistent, System.not_consistent_iff_inconsistent, System.inconsistent_iff_provable_bot]
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢! ⊥ → Nonempty (𝓣 ⊢' [])
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢! ⊥ → Nonempty (𝓣 ⊢' [])
Tactic:
rintro ⟨Δ, h, d⟩
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
⊢ Nonempty (𝓣 ⊢' [])
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
⊢ Nonempty (𝓣 ⊢' [])
Tactic:
have : Δ ⊢² [] := Cut.cut d (falsum _ _)
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
this : Δ ⊢² []
⊢ Nonempty (𝓣 ⊢' [])
Theorem: LO.Gentzen.consistent_iff_isEmpty
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
this : Δ ⊢² []
⊢ Nonempty (𝓣 ⊢' [])
Tactic:
exact ⟨toDisjconseq this h⟩
Proof state after:
no goals
Theorem: LO.Gentzen.inconsistent_iff_nonempty
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ System.Inconsistent 𝓣 ↔ Nonempty (𝓣 ⊢' [])
Tactic:
simp [←System.not_consistent_iff_inconsistent, consistent_iff_isEmpty]
Proof state after:
no goals
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ 𝓣 ⊢! p → System.Inconsistent (cons (~p) 𝓣)
Tactic:
rintro ⟨⟨Δ, h, d⟩⟩
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ System.Inconsistent (cons (~p) 𝓣)
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ System.Inconsistent (cons (~p) 𝓣)
Tactic:
simp [inconsistent_iff_nonempty]
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ Nonempty (cons (~p) 𝓣 ⊢' [])
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ Nonempty (cons (~p) 𝓣 ⊢' [])
Tactic:
exact ⟨⟨~p :: Δ, by simp; intro q hq; right; exact h q hq, negLeft d⟩⟩
Proof state after:
no goals
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ ∀ p_1 ∈ ~p :: Δ, p_1 ∈ cons (~p) 𝓣
Tactic:
simp
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ ∀ a ∈ Δ, a = ~p ∨ a ∈ 𝓣
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
⊢ ∀ a ∈ Δ, a = ~p ∨ a ∈ 𝓣
Tactic:
intro q hq
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
q : F
hq : q ∈ Δ
⊢ q = ~p ∨ q ∈ 𝓣
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
q : F
hq : q ∈ Δ
⊢ q = ~p ∨ q ∈ 𝓣
Tactic:
right
Proof state after:
case h
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
case h
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣
Tactic:
exact h q hq
Proof state after:
no goals
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ System.Inconsistent (cons (~p) 𝓣) → 𝓣 ⊢! p
Tactic:
letI := Classical.typeDecidableEq F
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons (~p) 𝓣) → 𝓣 ⊢! p
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons (~p) 𝓣) → 𝓣 ⊢! p
Tactic:
simp [inconsistent_iff_nonempty]
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons (~p) 𝓣 ⊢' [] → 𝓣 ⊢! p
Theorem: LO.Gentzen.provable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons (~p) 𝓣 ⊢' [] → 𝓣 ⊢! p
Tactic:
exact fun b ↦ ⟨b.deductionNeg⟩
Proof state after:
no goals
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ 𝓣 ⊢! ~p → System.Inconsistent (cons p 𝓣)
Tactic:
rintro ⟨⟨Δ, h, d⟩⟩
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ System.Inconsistent (cons p 𝓣)
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ System.Inconsistent (cons p 𝓣)
Tactic:
simp [inconsistent_iff_nonempty]
Proof state after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ Nonempty (cons p 𝓣 ⊢' [])
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ Nonempty (cons p 𝓣 ⊢' [])
Tactic:
exact ⟨⟨p :: Δ, by simp; intro q hq; right; exact h q hq, ofNegRight d⟩⟩
Proof state after:
no goals
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ p_1 ∈ p :: Δ, p_1 ∈ cons p 𝓣
Tactic:
simp
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ 𝓣
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ 𝓣
Tactic:
intro q hq
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q = p ∨ q ∈ 𝓣
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q = p ∨ q ∈ 𝓣
Tactic:
right
Proof state after:
case h
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
case h
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣
Tactic:
exact h q hq
Proof state after:
no goals
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p
Tactic:
letI := Classical.typeDecidableEq F
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p
Tactic:
simp [inconsistent_iff_nonempty]
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons p 𝓣 ⊢' [] → 𝓣 ⊢! ~p
Theorem: LO.Gentzen.refutable_iff_inconsistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons p 𝓣 ⊢' [] → 𝓣 ⊢! ~p
Tactic:
exact fun b ↦ ⟨b.deduction⟩
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_insert_iff_not_refutable
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ System.Consistent (cons p 𝓣) ↔ 𝓣 ⊬! ~p
Tactic:
simp [System.Unprovable, refutable_iff_inconsistent, System.not_inconsistent_iff_consistent]
Proof state after:
no goals
Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
A : System.Consistent 𝓣
⊢ False
Tactic:
have : 𝓣 ⊢' [] := Disjconseq.cut bp br
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
A : System.Consistent 𝓣
this : 𝓣 ⊢' []
⊢ False
Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
A : System.Consistent 𝓣
this : 𝓣 ⊢' []
⊢ False
Tactic:
exact (consistent_iff_isEmpty.mp A).false this
Proof state after:
no goals
Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable!
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢! p
br : 𝓣 ⊢! ~p
⊢ System.Inconsistent 𝓣
Tactic:
rcases bp with ⟨bp⟩
Proof state after:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
br : 𝓣 ⊢! ~p
bp : 𝓣 ⊢ p
⊢ System.Inconsistent 𝓣
Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable!
Proof state before:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
br : 𝓣 ⊢! ~p
bp : 𝓣 ⊢ p
⊢ System.Inconsistent 𝓣
Tactic:
rcases br with ⟨br⟩
Proof state after:
case intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
⊢ System.Inconsistent 𝓣
Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable!
Proof state before:
case intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
⊢ System.Inconsistent 𝓣
Tactic:
exact inconsistent_of_provable_and_refutable bp br
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
h : System.Consistent (System.theory 𝓣)
⊢ Collection.set 𝓣 ⊆ Collection.set (System.theory 𝓣)
Tactic:
simp [Set.subset_def]
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
h : System.Consistent (System.theory 𝓣)
⊢ ∀ x ∈ 𝓣, x ∈ System.theory 𝓣
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
h : System.Consistent (System.theory 𝓣)
⊢ ∀ x ∈ 𝓣, x ∈ System.theory 𝓣
Tactic:
intro p hp
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
h : System.Consistent (System.theory 𝓣)
p : F
hp : p ∈ 𝓣
⊢ p ∈ System.theory 𝓣
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
h : System.Consistent (System.theory 𝓣)
p : F
hp : p ∈ 𝓣
⊢ p ∈ System.theory 𝓣
Tactic:
exact System.Axiomatized.provable_axm  𝓣 hp
Proof state after:
no goals