Why do we require Hilbert spaces describing quantum systems to have a countable orthonormal basis

Question

It is postulated that a quantum system is (in part) represented by a separable Hilbert space. It seems that the actual (equivalent to separability) property of interest is that the Hilbert space has a countable orthonormal basis. Why is this postulated? What is wrong with an "uncountably infinite orthonormal basis"?

Answer 1

Sometimes it is assumed by hypothesis, but it is not strictly necessary actually, since all the formalism is valid in any cases. If the Hilbert space supports a strongly continuous irreducible unitary representation of a Lie group, then the space is separable. This happens in particular as a consequence of Stone von Neumann theorem, in non relativistic QM, when assuming that the space is an irreducible rep of the CCRs.