This question is motivated by the discussion in the comments to this post. The question concerns a comparison of model-theoretic (extension) approaches to nonstandard analysis, and axiomatic (syntactic) approaches such as IST, BST, HST, and others.
Consider the following two examples.
An internal subset of $\mathbb R^\ast$ which is already contained in $\mathbb R\subseteq \mathbb R^\ast$ is necessarily finite. The proof of this as found in a popular textbook such as Goldblatt's is somewhat involved. Meanwhile, in axiomatic set theories, the fact that an infinite set must contain nonstandard elements is immediate from Idealisation.
Overspill: every internal subset of $\mathbb N^\ast$ containing $\mathbb N$ must also contain a nonstandard integer, or equivalently an internal set containing all nonstandard integers must contain a standard integer. Proofs in the model-theoretic approach need to develop internal induction or internal well-ordering first, whereas in the axiomatic approach one just applies the usual well-ordering property of $\mathbb N$ to derive a contradiction from the existence of a set of all nonstandard integers.
Another example that occurred to me while I was preparing a recent talk is the integral. In model-theoretic approaches, one defines it as the shadow (i.e., standard part) of a suitable hyperfinite sum. To justify such a procedure, one needs to verify that hyperfinite sums indeed exist and behave as finite sums in a suitable sense. In the axiomatic approaches, the integral is the shadow of a finite sum as the index runs from 1 to $\mu$ (where $\mu$ is a nonstandard integer in $\mathbb N$), and no additional verifications are necessary.
I am looking for further examples of this type so as to illustrate the fact that sometimes axiomatic approaches have their advantages over the model-theoretic ones (and vice versa). The kind of examples I am looking for would preferably be applicable also to the weaker systems SPOT or SCOT. Note that, even though the axioms of SPOT do not include idealisation, one can actually prove countable Idealisation within SPOT.
Note. To answer some of the queries in the comments, the standard reference for axiomatic nonstandard analysis is Kanovei and Reeken where theories IST, BST, HST are presented in detail. The more recent theories SPOT and SCOT are outlined here with the appropriate links. Consistency: all of these theories are equiconsistent with ZF(C). Conservativity: all of these theories are conservative over ZFC. SPOT is conservative over ZF. SCOT is conservative over ZF+ADC. Interpretability: (not IST but) BST admits a standard core interpretation in ZFC (every model of ZFC is the "standard core" of a suitable model of BST). Multiverse: the Gitman-Hamkins "toy model" of the multiverse is compatible with BST in the sense that two adjacent universes have the property that the smaller one is the standard core of the larger one, as discussed here.
