Is there any physical system with a non-separable Hilbert space? It seems that all the usual physical systems have a separable Hilbert space. Is there any example with a non-separable Hilbert space? 
BTW, I am actually always baffled by the fact that a continuous model like the 1d harmonic oscillator defined on $\mathbb{R}$ has a separable Hilbert space. It is well known that $\mathbb{R}$ is uncountable. But on the other hand, the Hermite polynomials are countable. This means while the Hermite polynomials (with some Gaussian prefactor) are a legitimate basis of the Hilbert spade, the more common and sloppy coordinate basis $|x \rangle $ are not. 
 A: The standard formulations of QM and QFT are such that the resulting Hilbert space is always separable, namely there exist a finite or infinite countable Hilbert basis (and thus every Hilbert bases are of the same type correspondingly).
Separability is required as an axiom from scratch or it arises as a consequence of more basic axioms. In particular

*

*For elementary non-relativistic systems, all irreducible representations of $X_j$ and $P_k$ CCRs  produce separable Hilbert spaces $L^2(\mathbb R^n, d^nx)$ in view of the celebrated Stone-von Neumann theorem. Adding the spin does not alter the result because the space becomes $L^2(\mathbb R^n, d^nx) \otimes \mathbb C^{2s+1}$ which is still separable.


*If the elementary system is relativistic and therefore supports an irreducible unitary strongly-continuous representation of Poincaré group,separability  arises by the classification of the afore-mentioned representations which works on Hilbert spaces of the form  $L^2(\mathbb R^n, d^nk) \otimes \mathbb C^{2s+1}$.


*Finite composite systems are obtained by taking a finite tensor product of elementary systems, so that separability is preserved.


*In the absence of complicated phenomena as spontaneously broken symmetry (see below), assuming asymptotic completeness, QFT is defined in a Fock space constructed out of separable Hilbert spaces (one particle spaces). These Fock spaces are separable.


*In curved spacetime, at least in static spacetimes and using the static vacuum as vacuum of the Fock representation, separability is still guaranteed as the one particle space is still a $L^2$ space over a separable (in measure-theory sense) space.
Non separability may arise in presence of continuous superselection rules if picturing them as a direct sum instead of a cumbersome direct integral of sectors. Think of a non relativistic system admitting a mass operator $M$ whose spectrum $\sigma(M)$ is an interval, say $(a,b)$.  The Hilbert space results to be the direct orthogonal sum of an infinitely continuous class of eigenspaces $\cal H_m$ of the mass operator
$$\cal H = \oplus_{m \in \sigma(M)} \cal H_m$$
so that $\cal H$ cannot be separable as it admits an uncountable sequence of pairwise orthogonal subspaces.
Notice that the spectrum of $M$ is a pure point spectrum made of an interval $\sigma(M) = \sigma_p(M) =(a,b)$ in this picture. This fact is possible in spite of the name "point" spectrum, which is misleading here.
Here, if one admits that the system supports a (projecitve unitary)  representation of Galileo group, due to Bargmann's superselection rule of the mass, quantum physics is described in each subspace separately (in the standard way ${\cal H}_m = L^3(\mathbb R, d^3x)$ if the system is a particle with mass $m$ and $m$ appears therein as a fixed parameter) and at most incoherent superpositions of states of different subspaces are permitted.
In each such subspace ${\cal H}_m$ vectors are normalizable  and all observables $A$ of the theory admit every ${\cal H}_m$ as invariant subspace, since $A$ commutes with $M$.
The fact that the vectors in each ${\cal H}_m$ are normalizable  is the basic difference from the direct integral picture  where  vectors are instead similar to the kets $|x\rangle$ such that $\langle x| x \rangle$ does not make sense. In this representation $\sigma(M)$ is a continuous spectrum but the theory is quite singular in each coherent sector ${\cal H}_m$ which is not a subspace of the overall Hilbert space. As far as I remember a similar situation arises in loop quantum gravity...
Non-separability arises also when some symmetry  spontaneously  breaks and you consider all possible Hilbert spaces (continuously parametrized) as orthogonal subspaces of an overall Hilbert space.
Non separable Hilbert spaces have the pathology that quantum statistical mechanics cannot be formulated at least in the standard way, since the trace of usual statistical operators describing equilibrium necessarily diverges. This is because the overall Hamiltonian operator (if assuming to have pure point spectrum) admits an uncountable basis of eigenvectors. Though, in each superselection sector no problem arises.
In presence of non separable Hilbert spaces perhaps the algebraic approach seems more suitable. Thermodynamical equilibrium may be described in terms of KMS condition for an algebraic  state over a C*-algebra of observables.
Non-separability arises from a very abstract viewpoint when considering all non unitarily equivalent representations of a given C*-algebra of observables, e.g., field operators referring to all possible vacua, in a unique Hilbert space made of all the GNS representations of these vacua.
Addendum. As I realized after a discussion with a colleague (at Les Houches school of physics)
separability of the Hilbert space arises as soon as the system admits (is) an irreducible strongly-continuous unitary representation of a  Lie group of symmetries.
(See the sketch of proof in the comments below.)
This includes both the case of a non-relativistic and relativistic particle mentioned above in particular.
A: I'll address your question about cardinality. (See also the excellent comments by Valter Moretti below.)
Let's say I have a countably infinite orthonormal (and hence linearly independent) set $S$ of vectors in an inner product space $V$, viz. $\left\langle m|n\right\rangle =\delta_{mn}$ with $m,\,n\in\mathbb{N}$. An infinite sequence of vectors whose $n$th element is $u_n:=a_n\left|n\right\rangle$ and $n$th partial sum is $S_n:=\sum_{k\le n}u_k$ satisfies $\left|S_m-S_n\right|^2= \sum_{k=n+1}^{m}\left|a_k\right|^2$ for $m\le n$. If our set is a "basis" of a Hilbert space in quantum mechanics, unitarity requires $\sum_n \left|a_n\right|^2=1$. Thus $\lim_{n\to\infty}\sum_{k=1}^{n}\left|a_k\right|^2=1$ and $\sum_{k=n+1}^{m}\left|a_k\right|^2\le 1-\sum_{k=1}^{n}\left|a_k\right|^2$ can be made arbitrarily small with sufficiently large $m,\,n$. Our sequence of $u_n$ is then a Cauchy sequence.
An inner product space is also a metric space. If each Cauchy sequence in a metric space (inner product space) has a limit therein, we call the space a complete metric space (Hilbert space). We use Hilbert spaces in quantum mechanics to ensure all unitary sums of vectors as above will exist as elements of the state space. Let's see what happens if we don't add the it's-Hilbert assumption.
Since $S$ spans a subspace $W$ of $V$, which may or may not be $V$ (in particular, there may or may not exist $S$ such that $W=V$), $W$ contains all linear combinations of finitely many elements of $S$. In fact, for general inner product spaces we define the span of $S$ as the set of vectors expressible in this form; if it's not Hilbert, we can't in general assume an infinite series has well-defined limit in $V$. The dimension theorem states all $S$ that span a given choice of $W$ have the same cardinality, which is called the dimension of $W$.
In Hilbert spaces, by contrast, we're allowed to use infinitely many members of a "basis" to form a sum; it will exist in the space as long as the coefficients satisfy unitarity. So, strictly speaking, a "basis" in the Hilbert-space sense isn't the type of basis described in the dimension theorem, whose proof (case 1 here) relies on the finitely-many-elements condition.
The Hilbert space that had you confused, viz. "is its dimension $\aleph_0$ or $c$?", is a good example of this subtlety. The countably infinite set of vectors that "span" it do so only with the machinery that makes Hilbert spaces special. In dimension-theorem terms, any "basis" of that space has cardinality $c$ because the countably infinite "Hilbert-basis" only "spans" (as opposed to "Hilbert-spans") a countably infinite subspace: namely, the set of vectors expressible using finitely many of its elements. (You can verify that set satisfies the definition of a vector space.) For example, this subspace contains $\sum_{k=1}^{10}\frac{1}{\sqrt{10}}\left| k\right\rangle$ but not $\sum_{k=1}^{\infty}\frac{\sqrt{6}}{k\pi}\left| k\right\rangle$, whereas the full Hilbert space contains both.
Note: none of the phrases I've placed in scare quotes are technical terms; they're just a way to emphasize here the difference between concepts with the same name.
