Theorem: LO.FirstOrder.ProvabilityPredicate.loeb_theorm (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
H : T ⊢! ⦍β⦎σ ⟶ σ
⊢ T ⊢! σ
Tactic:
have d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ := imp_trans! (Subtheory.prf! (kreisel_specAux₁ σ)) 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 ⊢! ⦍β⦎σ ⟶ σ
d₁ : 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 ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
⊢ T ⊢! σ
Tactic:
have d₂ : T ⊢! ⦍β⦎κ(σ)      := Subtheory.prf! (𝓢 := T₀) (D1 $ Subtheory.prf! (kreisel_specAux₂ σ) ⨀ d₁)
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 ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
d₂ : 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 ⊢! ⦍β⦎σ ⟶ σ
d₁ : T ⊢! ⦍β⦎κ(σ) ⟶ σ
d₂ : T ⊢! ⦍β⦎κ(σ)
⊢ T ⊢! σ
Tactic:
exact d₁ ⨀ d₂
State after:
no goals