An Automated Deduction of a 'Dishkant-Implication-Restricted' Foulis-Holland Theorem from Orthomodular Quantum Logic: Part 4

摘要

The optimization of quantum computing circuitry and compilers at some level must be expressed in terms of quantum-mechanical behaviors and operations. The algebra, C(H), of closed linear subspaces of (equivalently, the system of linear operators on (observables in)) a Hilbert space is a logic of the system of "measurement-propositions" quantum mechanical systems and is a model of an ortholattice (OL). An OL can thus be thought of as a kind of "quantum logic" (QL). C(H) is also a model of an orthomodular lattice (OML), which is an ortholattice to which the orthomodular law has been conjoined. An OML can thus be regarded as an orthomodular (quantum) logic (OMLogic). Now a QL can be thought of as a BL in which the distributive law does not hold. Under certain commutativity conditions, a QL does satisfy the distributive law; among the most well known of these relationships are the Foulis-Holland theorems (FHTs). Megill and Pavicic have defined variants of the QL "meet" and "join" connectives in terms of each of the five implication connnectives of QL; we can call these variant meet and join connectives "implication-restricted". Here I provide an automated deduction of one of the four Foulis-Holland theorems, restricted to "Dishkant" implication (one of the QL implication-connectives), from OML theory.