Theorem: LO.Gentzen.provable_iff_inconsistent (Logic/Logic/Calculus.lean)

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⟩⟩
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) 𝓣)

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]
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) 𝓣 ⊢' [])

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⟩⟩
State after:
no goals

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
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 ∈ 𝓣

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
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 ∈ 𝓣

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
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 ∈ 𝓣

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
State after:
no goals

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
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

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]
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

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⟩
State after:
no goals