suffices ¬(T ⊢! G ∨ T ⊢! ~G) by
  simpa[System.Undecidable, not_or] using this
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ Undecidable T G
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)