Theorem: LO.FirstOrder.ProvabilityPredicate.formalized_loeb_theorem (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✝ : β.HilbertBernays T₀ T
σ : Sentence L
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have hκ₁ : T₀ ⊢! ⦍β⦎(κ(σ)) ⟶ ⦍β⦎σ := kreisel_specAux₁ σ
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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
⊢ 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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ (⦍β⦎κ(σ) ⟶ σ) := imply_left_replace! hκ₁
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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
⊢ 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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
have : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ) := Subtheory.prf! (𝓢 := T₀) $ imp_trans! this (kreisel_specAux₂ σ)
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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this✝ : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
this : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ)
⊢ 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✝ : β.HilbertBernays T₀ T
σ : Sentence L
hκ₁ : T₀ ⊢! ⦍β⦎κ(σ) ⟶ ⦍β⦎σ
this✝ : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎κ(σ) ⟶ σ
this : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ κ(σ)
⊢ T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
Tactic:
exact imp_trans! (D2 ⨀ (D1 this)) hκ₁
State after:
no goals