Discrete quantum structures I: Quantum predicate logic

A discrete quantum structure is a discrete quantum space that is equipped with relations and functions of various finite arities. Discrete quantum spaces are identified with hereditarily atomic von Neumann algebras, their relations with projection operators, and their functions with unital normal *-homomorphisms. The propositional quantum logic of Birkhoff and von Neumann has been extended to a predicate quantum logic by Weaver; we investigate this predicate quantum logic as the internal logic of discrete quantum structures. We extend this predicate quantum logic to include function symbols and an equality symbol. Overall, we recover the basic structures of discrete quantum mathematics from physical first principles. More complicated structures will be recovered similarly in part II of this paper.