Axiomatic Quantum Theory

The basis of a rigorous formal axiomatization of quantum mechanics is constructed, built upon Dirac's bra–ket notation. The system is three-sorted, with separate variables for scalars, vectors and operators. First-order quantification over all three types of variable is permitted. Economy in the axioms is effected by, e.g., assigning a single logical function * to transform (i) a scalar into its complex conjugate, (ii) a ket vector into a bra and a bra into a ket, (iii) an operator into its adjoint. The system is accompanied by a formal semantics. Further papers will deal with vector subspaces and projection operators, operators with continuous spectra, tensor products, observables, and quantum mechanical probabilities.