Here we introduce the axioms a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. The 18 axioms for a complex Hilbert space consist of ax-hilex, ax-hfvadd, ax-hvcom, ax-hvass, ax-hv0cl, ax-hvaddid, ax-hfvmul, ax-hvmulid, ax-hvmulass, ax-hvdistr1, ax-hvdistr2, ax-hvmul0, ax-hfi, ax-his1, ax-his2, ax-his3, ax-his4, and ax-hcompl.
The axioms specify the properties of 5 primitive symbols, , , , , and .
If we can prove in ZFC set theory that a class is a complex Hilbert space, i.e. that , then these axioms can be proved as Theorems axhilex-zf, axhfvadd-zf, axhvcom-zf, axhvass-zf, axhv0cl-zf, axhvaddid-zf, axhfvmul-zf, axhvmulid-zf, axhvmulass-zf, axhvdistr1-zf, axhvdistr2-zf, axhvmul0-zf, axhfi-zf, axhis1-zf, axhis2-zf, axhis3-zf, axhis4-zf, and axhcompl-zf respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex-zf.