1
$\begingroup$

I need help understanding a counter-example in non-standard analysis. First a few preliminaries:

Def.: A Neutrix is a convex additive subgroup of the hyperreals ${}^*\mathbb R$.

The two simplest examples of non-trivial neutrices are the set of infinitesimals $\mathbb I$ and the limited numbers $\mathbb L$. Moreover if $N$ is a neutrix, then $\mathbb L N = N$ and $C N$ is also a neutrix for any convex set $C$. Note that besides $\{0\}$ and ${}^*\mathbb R$ itself, neutrices are always external sets.

Question: Given a neutrix $N$, does there always exist a sequence $a_n$ of hyperreals such that $N$ is equal to the countable union or intersection

$$ N = \bigcup_{n\in\mathbb N} (-a_n,+a_n) \qquad\textbf{or}\qquad N = \bigcap_{n\in\mathbb N} (-a_n,+a_n) $$

For example $\mathbb L = \bigcup_{n\in\mathbb N} (-n,+n)$ and $\mathbb I = \bigcap_{n\in\mathbb N} (-\frac{1}{n},+\frac{1}{n})$.

In his book Nonstandard Asymptotic Analysis, Imme van den Berg provides a counter-example that I don't understand; my biggest problem is that he works with Nelson's Internal Set Theory (IST) and I don't know how to properly translate it into Robinson's framework.

Let $w\in\mathbb R^+$ be unlimited and let $F$ be the set of all increasing real functions. Then $$ G_w = \{x\in\mathbb R | \exists f\in F^\text{st} : 0\le x\le f(w)\}$$ where $F^\text{st} = \{f\in F| f\text{ standard}\}$, is a strictly generalized galaxy. I.e. $G_w$ is external set of the form $G_w = \bigcup_{x\in X^\text{st}} A_x$ for a internal family $\{A_x\}_{x\in X}$ of internal sets, where $X$ must be uncountable (= strict).

Proof: (1): $G_w$ is external because on one side it is obviously a convex additive semigroup of $\mathbb R^+$, but then again $G_w\neq \mathbb R^+$ since by the idealization principle applied on the formula $$ B(f,y) \iff f\in F \wedge f(w)<y $$ it follows that there exists $y\in\mathbb R^+$ with $y>G_w$.

(2): $G_w$ is strict: Assume this would not be the case. Then, w.l.o.g., there exists a sequence of increasing standard functions $(f_n)_{n\in\mathbb N^\text{st}}$ such that $f_{n+1}$ dominates $f_n$ with $$G_w = \bigcup_{n\in\mathbb N^\text{st}} [0,f_n(w)] $$ Then by the lemma of du Bois-Reymond there exists an increasing standard function $g$ that dominates all $f_n$ for large inputs, i.e. $\forall n \exists a_n \forall x\ge a_n : g(x)>f_n(x)$. But then both $g(w)\in G_w$ and $g(w)>G_w$, contradiction!

So as far as I understand it - and correct me if I'm wrong - the set $F$ corresponds to the set of internal increasing functions ${}^*\mathbb R \to {}^*\mathbb R$ and a standard function $f\colon\mathbb R\to\mathbb R$ in IST corresponds to a hyperreal function ${}^*f\colon {}^*\mathbb R \to {}^*\mathbb R$ where ${}^*f$ is the canonical extension of a real function $f\colon\mathbb R\to\mathbb R$ to the hyperreals, hence $$G_w = \{x\in {}^*\mathbb R | \exists f\colon \mathbb R \to \mathbb R \text{ increasing} : 0\le x\le {}^*f(w)\} $$

Now the idealization principle says that if for any finite collection $\{f_1,\ldots,f_k\}\subset F^\text{st}$ there exists $y$ such that $B(f_1,y),\ldots,B(f_k,y)$ is true, then there exists $\hat y$ such that $B(f,\hat y)$ is true for all $f\in F^\text{st}$.

However on the other side it is trivial to construct, for any given $y\in {}^*\mathbb R^+$, an increasing function $f\colon\mathbb R\to\mathbb R$ such that ${}^*f(w)>y$: if $y = [y_k]$ and $w =[(1,2,3,\ldots)]$, simply pick $f$ such that $f(k) > y_k$ for all $k$. So $G_w = {}^*\mathbb R^+$

What am I missing?

$\endgroup$
0
$\begingroup$

I haven't checked all the details but the last part of your argument seems to assume that the hyperreals are the ordinary ultrapower over a countable index set. This however is not enough to be a counterpart of the reals in Nelson's framework. One needs a much vaster construction to get a model sufficient for Nelson's purposes. This is reportedly done in an appendix to Nelson's paper though I have never read that.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.