Is the (first order theory) of Hilbert spaces categorical?

Question

Suppose the axioms of a Hilbert space (i.e. vector space, inner product, completeness and separability) are formulated as a first order theory.

It can be shown that any infinite dimensional Hilbert space is isomorphic to $l^2$ (the space of infinite sequences of complex numbers the sum of whose absolute squares converges). In other words, any model satisfying the (infinite dimensional) Hilbert space axioms is isomorphic to $l^2$.

1. Since all the models are isomorphic to $l^2$ (and hence to each other), the Hilbert space theory is categorical.

2. But by Lowenheim-Skolem theorem, any first order theory that has an infinite model of cardinality c, also has a model of any cardinality larger c.

So 2 seems to contradict 1, since all models of a categorical theory have to have the same cardinality (in order to be isomorphic).

How is this resolved?

Answer 1

It is not clear how to axiomatize Hilbert spaces in first-order logic. Do you use a two sorted language? How do you formalise completeness?

So, the easy answer is NO. Because it is ill-posed.

There is a more interesting YES answer if you turn to continuous logic. Then Hilbert spaces are uncountably categorical. You need to define categoricity in the right way.

An accessible reference for continuous logic is www.math.uiuc.edu/~henson/cfo/mtfms.pdf

Answer 2

There's an easy negative answer regardless to the way you want to think about it as a first-order structure:

If $\kappa$ is an infinite cardinal such that $\operatorname{cf}(\kappa)=\aleph_0$ then there is no Banach space of cardinality $\kappa$.

This is due to the Baire Category Theorem, and the fact that any subspace of smaller dimension is nowhere dense. If $\dim V$ has countable cofinality, then it's the increasing union of countably many subspaces of smaller dimension. Therefore $V$ couldn't be a Banach space, and in particular a Hilbert space.

In particular this means that whether you formalize Hilbert spaces in a two-sorted logic (which will allow you to generate countable models) or an uncountable language (which will ensure that all models are rather large, but you can always make them arbitrarily large), you can't have a Hilbert space of size $\beth_\omega$. So it's impossible to have a first-order theory for Hilbert spaces.

On the other hand, the interesting question would be if you formalize Hilbert spaces as a first-order two-sorted logic, and say that a first-order Hilbert space is a structure of this language with the same theory as $\ell_2$, (1) is this really the theory of all Hilbert spaces? and (2) is there a nice axiomatization for this theory (like there is for the real numbers)?

Answer 3

It is a bit of a moot point whether you include separability in the axioms for a Hilbert space. If you do, and you also require the space to be infinite dimensional, then you get the notion of the Hilbert space (e.g., as represented by $l_2$) that you will find in the early literature on the subject. However, I think it is more usual these days not to require separability, so we tend to talk about Hilbert spaces.

In any case, there is no obvious way to express completeness (or separability) as a first order property. The paper Some new results on decidability for elementary algebra and geometry by Bob Solovay, John Harrison and myself (subsequently published in the APAL) is mainly concerned with questions of decidability, but does include some results about axiomatizability. Specifically, Corollary 35 characterizes the axiomatizable classes of inner product spaces and implies that the class of Hilbert spaces and the class of separable Hilbert spaces are not axiomatizable. This proves that there really is no way of expressing completeness using first order axioms.

Our paper is couched in terms of a two-sorted presentation of inner product spaces and normed metric spaces with a sort for scalars and a sort for vectors, but this is only a technical convenience. It is tedious but not difficult to encode the two-sorted language in an ordinary single-sorted first order language, in which the universe is taken to include both the scalars and the vectors and you have one-place predicates that single out the scalars and the vectors.