Quantum First-Order Logics that Capture Logarithmic-Time/Space Quantum Computability

We introduce a quantum analogue of classical first-order logic (FO) and develop a theory of quantum first-order logic (QFO) as a basis of the productive discussions on the power of logical expressiveness of QFO toward quantum computing. The purpose of this work is to logically express “quantum computation” by introducing specially-featured quantum connectives and quantum quantifiers that quantify fixed-dimensional pure quantum states. Our approach is founded on the schematic definitions of time-bounded quantum functions [J. Symb. Log. 85, 1546–1587] and quantum quantifiers for Quantum NP [Proc. IFIP TCS 2002, 323–336]. We demonstrate that quantum first-order logics possess an ability of expressing quantum logarithmic-time computability by the use of new “tabular” quantum variables. In contrast, an extra use of quantum transitive closure operators also helps us characterize quantum logarithmic-space computability.