Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_GL (Logic/Modal/Standard/Provability/Basic.lean)

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ ∀ {f : realization L α}, T ⊢! f[β] p
Tactic:
apply arithmetical_soundness_K4Loeb (T₀ := T₀)
State after:
case h
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p

State before:
case h
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Tactic:
exact (System.reducible_iff.mp reducible_GL_K4Loeb) h
State after:
no goals