Theorem: LO.FirstOrder.ProvabilityPredicate.unprovable_consistency_of_Loeb (Logic/FirstOrder/Incompleteness/ProvabilityCondition.lean)

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ Consistent T → T ⊬! ~⦍β⦎⊥
Tactic:
contrapose
State after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ ¬T ⊬! ~⦍β⦎⊥ → ¬Consistent T

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
⊢ ¬T ⊬! ~⦍β⦎⊥ → ¬Consistent T
Tactic:
intro hC
State after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : ¬T ⊬! ~⦍β⦎⊥
⊢ ¬Consistent T

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : ¬T ⊬! ~⦍β⦎⊥
⊢ ¬Consistent T
Tactic:
simp [neg_equiv'!] at hC
State after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
⊢ ¬Consistent T

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
⊢ ¬Consistent T
Tactic:
have : T ⊢! ⊥ := Loeb.LT T₀ hC
State after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ ¬Consistent T

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ ¬Consistent T
Tactic:
apply System.not_consistent_iff_inconsistent.mpr
State after:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ Inconsistent T

State before:
L : Language
inst✝⁴ : DecidableEq (Sentence L)
inst✝³ : Semiterm.Operator.GoedelNumber L (Sentence L)
T₀ T : Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.Loeb T₀ T
hC : T ⊢! ⦍β⦎⊥ ⟶ ⊥
this : T ⊢! ⊥
⊢ Inconsistent T
Tactic:
apply System.inconsistent_of_provable this
State after:
no goals