Are there any examples of quantum logic being applied to solve actual physical questions, in particular to predict the physical properties (spectrum etc.) of some quantum-mechanical system? (Note that I'm not considering applications in quantum computing here.)


EDIT: To clarify what I mean, consider a simple system like the harmonic oscillator. Using real variables $q\_t$ and $p\_t$ indexed by real-valued time $t$, and starting from energy conservation in a form like $\forall t\forall s p\_s\cdot p\_s+\omega\cdot\omega\cdot q\_s\cdot q\_s=p\_t\cdot p\_t+\omega\cdot\omega\cdot q\_t\cdot q\_t$ and from the relation $\dot{q}=p$ expressed using a form "$\forall\epsilon\ldots<\epsilon$", I have no doubt that most of the properties of the classical system could be laboriously derived using the axioms for the real numbers and classical logic. (Of course if I'm wrong and there is some obstacle that means that solving even such a simple dynamical system cannot be logically formalized, that would be an interesting answer, too!) Has anyone ever tried to derive the properties of the corresponding quantum system using some appropriate form of quantum logic?



Physics applications of quantum logic
I'm fairly confident that there are no such derivations, and for good reason.


The paper I like on this topic is by Michael Dunn, [Quantum Mathematics](https://philpapers.org/rec/DUNQM). He concludes



> 
> First-order Peano arithmetic formulated with quantum logic has the
>  same theorems as classical first-order Peano arithmetic. Distribution
>  for first-order arithmetical formulas is a theorem not of quantum
>  logic but rather of arithmetic.
> 
> 
> 


He also gets a similar result for extensional second-order arithmetic.


So if the energy conservation is formalized in any Dunn-like extensional system, it will have the same consequences using either classical logic or quantum logic.


Getting different results from quantum logic would be a tall order -- especially since quantum logic is a subsystem of classical logic. This would presumably require:


* 1) A decision to model the physical system using some axiomatics which are consistent under quantum logic but inconsistent under classical logic.
* 2) A formalized treatment of real numbers and functions under quantum logic, sufficiently advanced to allow discussion of derivatives, which does not give the same theorems as classical mathematics.


Success might look like a quantum analog of synthetic differential geometry, which uses intuitionist logic. This is indeed sufficiently advanced to allow discussion of derivatives, inconsistent with classical logic (violating $\forall x (x=0 \vee x\neq 0)$), and giving different theorems from classical mathematics (e.g. $\forall x(\forall y(y^2=0 \rightarrow xy=0)\rightarrow x=0$).


I've tried my hand at finding that quantum treatment of real numbers and functions, without success, and so far as I can tell no one else has had success either.


