I am exploring areas where non-standard analysis or the theory of surreal numbers has yielded results that remain exclusive to these frameworks without analogs or proofs in classical analysis. For example, Robinson's proof regarding polynomially compact linear operators on Hilbert spaces eventually found its translation into classical terms. Are there other significant theorems or results in non-standard analysis or surreal numbers that have not been similarly translated or reconciled with traditional methods in classical analysis?
While there is a transfer principle, I am curious if there are known results that explicitly rely on higher-order logic or other aspects outside the scope of the transfer principle? Or maybe even results in the first-order logic, but without standard proof, because as far as I understand the complexity of the proof can be exponentially increased. Examples or discussions on this topic would be greatly appreciated.