SOME CRITICISMS OF QUANTUM LOGIC.

J. Harrison

Thomas A. Brody

Alireza Moazzen

This article employs a descriptive-analytical method with an algebraic and axiomatic approach to address quantum logic. Through several thought experiments, it is demonstrated that the distributive law for propositions does not hold in quantum mechanics. Therefore, the logic governing this domain of science is not classical logic. In fact, the algebra corresponding to the logic of quantum propositions is an orthomodular lattice, which is why the distributive law is not necessarily valid for such propositions. In quantum logic, various definitions are offered for the implication operator. Since none of these operators satisfy the deduction theorem, a suitable implication operator with this property must be defined. This objective is achieved by defining a unified quantum logic. By constructing a Lindenbaum-Tarski algebra for this unified quantum logic, it can be shown that it is indeed a quantum logic. Dishkant presented an embedding of quantum logic into the Br-modal logic system. This provides an appropriate semantics for quantum logic. A suitable model for this logic is the closed subspaces of a Hilbert space.

Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata

While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. Therefore, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. We have proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. However, BDQL does not support concurrency in its formalization. This article introduces Concurrent Dynamic Quantum Logic (CDQL), an extension of BDQL, to formalize and verify concurrent models of quantum protocols. CDQL is more expressive than BDQL by considering concurrent behavior and communication among participants in quantum protocols. Since CDQL is a conservative extension of BDQL, we extend the syntax of BDQL to CDQL and make a transformation from CDQL to BDQL without interrupting the semantics of BDQL. We also extend the implementation of BDQL to support CDQL, making a new support tool in Maude. The new support tool is equipped with a lazy rewriting strategy to make the verification process significantly faster. Several quantum communication protocols are successfully formalized and verified in BDQL/CDQL, demonstrating the effectiveness of our automated approach and tool in verifying quantum protocols.

Thomas A. Brody