File Marsden-Herman_Theorem.pdf contains a Mathematica-based automated derivation of the Marsden-Herman Theorem (MHT) of quantum logic. Informally, the MHT says that if there is a cyclic chain of four commuting elements in an orthomodular lattice, the distributive law holds for those elements
We can think of the set of propositions describing the outcome of measurements of physical systems as a set of propositions of the form “”Measurand X had (didn’t have) value V at time t”. In classical physics, this system of propositions has a Boolean logic (BL). In quantum mechanics, in contrast, the system of propositions describing the outcome of measurements of physical systems is isomorphic to the algebra, C(H), of closed linear subspaces of (equivalently, the system of linear operators on (observables in)) a Hilbert space and is a model of an ortholattice (OL). An OL can thus be thought of as a kind of “quantum logic” (QL). A consequence of the existence of non-commuting observables in quantum mechanics is that QL does not satisfy the BL distribution law. Quantum logicians have thus paid much attention to “quasi”-distributive theorems, one of the better known of which is the Foulis-Holland Theorem. A Mathematica-Based Deduction of the Foulis-Holland Theorem in Quantum Logic is an automated deduction of the FHT.
The paper at the link in the predecessor paragraph was last modified on 29 February 2020/0945 US Central Time.
This page was last updated on 1 October 2019/1515 US Central Time.