Hilbert Space axiom in QM My question is about the standard axiom on Hilbert's space in orthodoxal QM. It seems that this axiom appeares actually as an external pure mathematical axiom in all textbooks. Say, Mackey introduces it in his books as the axiom 7 and remarks about its substantiation like "why ... it works well". I'm wonder is it possible, based on some principal physical argument, to derive it? I know that Ludwig's book on QM has a subtitle to its 1st volume like a "derivation of Hilbert space structure". But it is very difficult to force one's way through his arguments. 
 A: It is actually possible to improve Mackey's approach completing a program started in the seventies by Jauch and Piron.
I remind you that a lattice is a partially ordered set $(\cal L, \leq)$
such that for every pair $a,b \in \cal L$ there exist
$$ a\vee b := \sup\{a,b\}\in \cal L \quad \quad \mbox{and}\quad \quad a\wedge b := \inf\{a,b\}\in \cal L$$
Let us assume that the elementary propositions $p,q,\ldots$ of a quantum system, which can be experimentally tested producing the outcomes "Yes/No",  give rise to the mathematical structure of a partially ordered set, where the order relation $p \leq q$ is the logical implication $p$ => $q$. 
The family  of all testable elementary propositions of a quantum system   is actually an orthomodular, atomic, separable, irreducible lattice satisfying the so called covering property and all these features  can be experimentally justified from the  quantum phenomenology (some of them were already justified in Mackey's textbook where, essentially, only the structure of partially ordered set is exploited). 
If the lattice includes at least four orthogonal atoms (*), it is possible to prove (theorem by Piron) that it coincides with the lattice of linear subspaces of a structure similar to the one of a Hermitian-scalar product  vector space where the field of complex numbers is generalized to a division ring equipped with an involution and a sort of non-singular (Hermitian) scalar product is given. The order relation of the lattice is the theoretical set inclusion of subspaces. 
The mentioned relevant subspaces $M$ forming the lattice are the ones closed (Maeda-Maeda theorem) with respect to  the notion of orthogonal $\neg$ (corresponding to the orthocomplement of the lattice), $M = \neg (\neg M)$. 
In this context $M \vee N$ is the closed subspace generated by $M$ and $N$ and $M \wedge N$ is the intersection of $M$ and $N$.
If, eventually, this vector space includes an infinite orthogonal system with constant norm, in view of the so-called Soler theorem (1995), the vector space can be proved to be a separable Hilbert space $H$ over $\mathbb R$, $\mathbb C$ or the division algebra of quaternions $\mathbb H$ and there is no further possibility. 
The so constructed lattice of elementary propositions is nothing but the lattice ${\cal L}(H)$ of orthogonal projectors over $H$ since there is a one-to-one correspondence between closed subspaces and orthogonal projectors in a Hilbert space over $\mathbb R$, $\mathbb C$ or $\mathbb H$.
A quantum observable $A$ is nothing but a collections of such projectors $\{P_E\}$ parametrized by sets $E\subset \mathbb R$ denoting the set where the outcome of the measurement of $A$ stays. 
$A$ is realized as a self-adjoint operator by just integrating its corresponding collection of elementary propositions (the physical meaning of the spectral theorem is just this one).
Here, a state is viewed as a probability measure over the lattice of orthogonal projectors. $\mu : {\cal L}(H) \ni P \mapsto \mu(P) \in [0,1]$.
The famous Gleason theorem, generalized by Varadarajan  to the quaternionic case, establishes that any such measure $\mu$ is a statistical operator $\rho_\mu$ and
$$\mu(P) = tr(\rho_\mu P)\quad \forall P \in {\cal L}(H)\:.$$
The extremal elements of this set of states are one-to-one with unit vectors up to phases (signs or quaternionic phases) as the standard QM assumes.
(See also this answer of mine)

(*) An atom is a proposition $a$ such that there is no further proposition $p$ with $p\leq a$, barring the always false proposition ${\bf 0}$. Atoms are one dimensional subspaces at the end of the reconstruction procedure.
A: 
is it possible, based on some principal physical argument, to derive it?

No, not really. This has been one of the driving goals of the field of quantum foundations for multiple decades, but as yet we don't know of any substantially simpler, more intuitive, or even different principle from which to derive the linearity axiom of quantum mechanics. 
We do know of a number of simpler and equivalent formulations, but they all produce equivalent theories and they have the weirdness embedded in some other part of the theory. The heart of the issue is that reality itself is weird, i.e. that matter exhibits wavelike behaviour including interference effects, and we know of no better way to phrase this than as the linear structure of Hilbert space.
If we do find a way to derive quantum mechanics from a simpler physical principle (in a way that is consistent with all of current experiments and known constraints, and which is validated by experiment itself) then trust me, you'll hear about it.
A: Hilbert spaces are needed because there exists physical systems that possess infinitely many eigenstates.
