Axiomatic quantum theory

The basis of a rigorous formal axiomatization of quantum mechanics is const ructed, built upon Dirac's bra-ket notation. The system is three-sorted, wi th separate variables for scalars, vectors and operators. First-order quant ification over all three types of variable is permitted. Economy in the axi oms is effected by, e.g. assigning a single logical function * to function (i) a scalar into its complex conjugate, (ii) a ket vector into a bra a a b ra into a ket, (iii) an operator into its adjoint. The system is accompanie d 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.