I have been trying to understand "The Hanf number of the first order theory of Banach spaces" by Shelah and Stern (Trans. AMS 244 (1978) 147-241). They construct a normed space $M$ from a Hilbert space $\cal H$ by taking the unit ball of $M$ to be the intersection of that of $\cal H$ with the halfspaces defined by $(x, \pm a) \le 1 - \delta_a$ for certain unit vectors $a$ and small $\delta_a >0$. They then need to show that the $\cal H$-unit ball is definable in $M$ using a first order language with symbols for vector addition and membership of the $M$-unit ball. With this in view, in their Lemma 2.9, they claim certain of the vectors $a$ are definable, but they don't have what they need to apply the lemma they appeal to for this (they have an inequality $\|b\| \le (1 - \delta)^{-1}$ but their Lemma 2.3 needs the opposite inequality).
So this looks like a bug. I suspect it can be fixed, e.g., by taking the unit ball to be the convex hull of the proposed one and the vectors $\pm a$. But this would be quite disruptive to the rest of the argument, I suspect.
My questions are (1) have I missed something so that Shelah and Stern's proof does actually go through more or less as its stands, or (2) is there another reference that gives a correct proof of these results.
