Theorem: LO.Gentzen.consistent_theory_iff_consistent (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
h : System.Consistent (System.theory 𝓣)
⊢ Collection.set 𝓣 ⊆ Collection.set (System.theory 𝓣)
Tactic:
simp [Set.subset_def]
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 𝓣

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

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
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
consis : System.Consistent 𝓣
⊢ System.theory 𝓣 ⊬! ⊥
Tactic:
rintro h
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
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ False

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
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ False
Tactic:
have : System.Inconsistent 𝓣 := System.inconsistent_iff_provable_bot.mpr <| System.StrongCut.cut! (by simp) h
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
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
this : System.Inconsistent 𝓣
⊢ False

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
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
this : System.Inconsistent 𝓣
⊢ False
Tactic:
exact System.not_inconsistent_iff_consistent.mpr consis this
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
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ 𝓣 ⊢!* Collection.set (System.theory 𝓣)
Tactic:
simp
State after:
no goals