Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_second (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
H : T ⊬! ~Con⦍β⦎
⊢ T ⊬! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
Tactic:
by_contra 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
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
⊢ False

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
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
⊢ False
Tactic:
have : T ⊢! ~Con⦍β⦎ := Loeb.LT T₀ $ contra₁'! 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
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
this : T ⊢! ~Con⦍β⦎
⊢ False

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
H : T ⊬! ~Con⦍β⦎
hC : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)
this : T ⊢! ~Con⦍β⦎
⊢ False
Tactic:
contradiction
State after:
no goals