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

Abstract

We introduce a quantum analogue of classical first-order logic (FO) and develop a theory of quantum first-order logic as a basis of the productive discussions on the power of logical expressiveness 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 quantum states. Our approach is founded on the recently introduced recursion-theoretical schematic definitions of time-bounded quantum functions, which map finite-dimensional Hilbert spaces to themselves. The quantum first-order logic (QFO) in this work therefore looks quite different from the well-known old concept of quantum logic based on lattice theory. We demonstrate that quantum first-order logics possess an ability of expressing bounded-error quantum logarithmic-time computability by the use of new "functional" quantum variables. In contrast, an extra inclusion of quantum transitive closure operator helps us characterize quantum logarithmic-space computability. The same computability can be achieved by the use of different "functional" quantum variables.

(A4, 10pt, 27 pages, 2 figures) This is a complete and corrected version of an extended abstract appeared in the Proceedings of the 20th Conference on Computability in Europe (CiE 2024), Amsterdam, the Netherlands, July 8-12, 2024, Lecture Notes in Computer Science, vol. 14773, pp. 311-323, Springer, 2024