Theorem: LO.FirstOrder.ProvabilityPredicate.kreisel_spec (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:
convert (diag (T := T₀) “x | !β.prov x → !σ”)
State after:
case h.e'_5.h.e'_4
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
⊢ ⦍β⦎κ(σ) ⟶ σ = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom ([→ #0].hom β.prov ⟶ [→ ].hom σ)

State before:
case h.e'_5.h.e'_4
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
⊢ ⦍β⦎κ(σ) ⟶ σ = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom ([→ #0].hom β.prov ⟶ [→ ].hom σ)
Tactic:
simp [kreisel, ←Rew.hom_comp_app, Rew.substs_comp_substs]
State after:
case h.e'_5.h.e'_4
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
⊢ ⦍β⦎fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ) = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom β.prov

State before:
case h.e'_5.h.e'_4
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
⊢ ⦍β⦎fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ) = [→ ⸢fixpoint T₀ ([→ #0].hom β.prov ⟶ [→ ].hom σ)⸣].hom β.prov
Tactic:
rfl
State after:
no goals