Editing Quantum logic (section)

== Algebraic structure ==
Quantum logic can be axiomatized as the theory of propositions modulo the following identities:{{sfn|Megill|2019}}
* ''a'' {{=}} &not;&not;''a''
* &or; is [[commutative]] and [[associative]].
* There is a maximal element ⊤, and ⊤ {{=}} ''b''&or;&not;''b'' for any ''b''.
* ''a''&or;&not;(&not;''a''&or;''b'') {{=}} ''a''.

("&not;" is the traditional notation for "[[negation (logic)|not]]", "&or;" the notation for "[[or (logic)|or]]", and "&and;" the notation for "[[and (logic)|and]]".)

Some authors restrict to [[orthomodular lattice]]s, which additionally satisfy the orthomodular law:<ref>{{harvnb|Kalmbach|1974}} and {{harvnb|Kalmbach|1983}}</ref> 
* If ⊤ {{=}} &not;(&not;''a''&or;&not;''b'')&or;&not;(''a''&or;''b'') then ''a'' {{=}} ''b''.

("⊤" is the traditional notation for [[truth]] and ""⊥" the traditional notation for [[Deception|falsity]].)

Alternative formulations include propositions derivable via a [[natural deduction]],{{sfn|Dalla&nbsp;Chiara|Giuntini|2002}} [[sequent calculus]]<ref>{{cite journal | jstor  = 44084050 | author1=N.J. Cutland |author2= P.F. Gibbins | title=A regular sequent calculus for Quantum Logic in which ∨ and ∧ are dual | journal=Logique et Analyse |series=Nouvelle Série | volume=25 | number=99 | pages=221–248 | date=Sep 1982 }}</ref><ref>
* {{cite journal | author=Hirokazu Nishimura | title=Proof theory for minimal quantum logic I | journal=International Journal of Theoretical Physics | volume=33 | number=1 | pages=103–113 | date=Jan 1994 |bibcode = 1994IJTP...33..103N |doi = 10.1007/BF00671616 | s2cid=123183879 |ref=none}}
* {{cite journal | author=Hirokazu Nishimura | title=Proof theory for minimal quantum logic II | journal=International Journal of Theoretical Physics | volume=33 | number=7 | pages=1427–1443 | date=Jul 1994 | doi=10.1007/bf00670687| bibcode=1994IJTP...33.1427N | s2cid=189850106 |ref=none}}</ref> or [[method of analytic tableaux|tableaux]] system.<ref>{{cite conference|url=http://www.kr.tuwien.ac.at/staff/tompits/papers/tableaux-99.pdf |author1=Uwe Egly |author2=Hans Tompits |title=Gentzen-like Methods in Quantum Logic |conference=8th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) |publisher=[[SUNY Albany]] | year=1999 |citeseerx=10.1.1.88.9045 }}</ref>  Despite the relatively developed [[proof&nbsp;theory]], quantum logic is not known to be [[decidability (logic)|decidable]].{{sfn|Megill|2019}}