theorem LO.ProvabilityLogic.N.arithmetical_soundness {L : FirstOrder.Language} [L.ReferenceableBy L] [L.DecidableEq] {T U : FirstOrder.Theory L} [T ⪯ U] {𝔅 : Provability T U} {A : Modal.Formula ℕ} (h : Modal.N ⊢! A) {f : Realization 𝔅} : U ⊢! ↑f A