This question is motivated by the discussion in the comments to [this
post](https://mathoverflow.net/q/454016/28128).  The question concerns
a comparison of model-theoretic (extension) approaches to nonstandard
analysis, and axiomatic (syntactic) approaches such as
[IST](https://en.wikipedia.org/wiki/Internal_set_theory), BST, HST,
and others.

Consider the following two examples.

1. 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](https://scholar.google.com/scholar?cites=4118501315415182310)
is somewhat involved.  Meanwhile, in axiomatic set theories, the fact
that an infinite set must contain nonstandard elements is immediate
from Idealisation.

2. 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.

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](https://link.springer.com/book/10.1007/978-3-662-08998-9) where theories IST, BST, HST are presented in detail.  The more recent theories SPOT and SCOT are outlined [here](https://u.math.biu.ac.il/~katzmik/spot.html) 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) BSF 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](https://u.math.biu.ac.il/~katzmik/infinitesimals.html#17f).  Please let me know if I missed anything.