# Comparison of model-theoretic and axiomatic approaches to NSA

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.

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

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

• What are BST, HST, SPOT, and SCOT? Sep 12 at 17:20
• I would find it important to inquire to what extent the nonstandard theories are mutually interpretable or bi-interpretable with the corresponding standard theories. It seems that ZFC is likely bi-interpretable with a suitable nonstandard theory, simply by interpreting via suitable iterated ultrapowers of V. If the theories are bi-interpretable, then they are arguably semantically equivalent variations of same underlying subject. It would be fruitless to argue for one over the other in this case except on style or convenience. So what is the interpretability status of these theories? Sep 12 at 23:21
• @VladimirKanovei Where are good references for these theories? Google is failing me. Sep 13 at 1:53
• @Noah: ""How do you justify taking an axiomatic approach without first knowing that (under mild assumptions) the relevant theory is consistent? To me it seems that the examples of 'axiomatic efficiency' in this question are just hiding the (usually model-theoretic) work elsewhere." This is a good objection, but notice that it only makes sense if you postulate that the appropriate starting point is an \in-theory, rather than a st-\in theory. The point I would like to make is that ... Sep 13 at 10:35
• ... the standardness predicate is not some kind of exotic post-modern innovation that must necessarily be viewed as superstructure to the "normal" set theory. My evidence for this is that the assignable/inassignable distinction was already in Leibniz, so it is arguably natural enough to be included as part of the axiomatic background. In other words, once the conservativity of the st-\in-theories are justified by what Schweber refers to as "model-theoretic work", it becomes clear that the st-\in-language is as legitimate as the \in-language rather than being some kind of stepchild. Sep 13 at 10:36