What is the (propositional) logic associated with an orthomodular lattice? In Quantum Mechanics the space of projections on the associated Hilbert Space of States forms an Orthomodular Lattice. Von Neumann calls this a Quantum Logic. When projections commute they generate a classical logic.
Now the Lindenbaum-Tarski construction gives an equivalence between classical propositional logic and boolean algebras.
Quantum Logic can be indentified as an orthomodular lattice. This means that the complement is also an involution, and that it is modular.
I'm hoping that the construction can be generalised to this context, in which case what kind of logic is associated with the orthomodular lattices?
 A: I use Polish notation.  C denotes a conditional, E logical equivalence, A disjunction, K conjunction, and N negation.  The correctness of this answer depends on the unary functions (or equivalently "functors") of quantum propositional logic.  I don't know what those are, but I would feel surprised if the method I get to in this answer would fail.
There exists a lemma [at least I hope I can invoke it here] which says that "if x=y, then Exy" where E comes as logical equivalence.  I'll use the equational axioms here for an orthomodular lattice.  Consequently, it follows that any axiomatization for an orthomodular lattice propositional logic will satisfy
commutation of disjunction  1 E Aab Aba

association of disjunction  2 E AAabc AaAbc

Double negation equivalence 3 E NNa a

A-K absorption              4 E AaKab a

Petrus Hispanus NANaNb-K    5 E NANaNb Kab

Modular Lattice Law         6 E Aab A[ K (Aab) Nb] b

What would come as a rule of inference?  We can't use {E$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$ since all of the above axioms don't have "E" as the principal connective of the antecedent.  So, structurally speaking, what do equations allow us to do?  They allow us to replace one proper or improper subformula $\zeta$ with another $\epsilon$ where $\zeta$=$\epsilon$.  There does exist a way to get the same ability to replace one proper or improper subformula with a logically equivalent one in a propositional calculus without using logical equivalence E.  So, even though the above six well-formed formulas won't work as an axiom set, they still come as useful for finding at least one possible axiom set.
Let $\delta$ denote a variable function of one argument.  There's a propositional law, which Lukasiewicz called "the law of extensionality", which says that C Epq C $\delta$ p $\delta$ q (Lukasiewicz got his understanding of these ideas from Lesniewski).  Now you can make substitutions for variable functions.  I'll outline how to know when you can do this in the last part of this answer.  It also holds that given detachment, that "if "if C  $\delta$ p  $\delta$ q", then "if C  $\delta$q  $\delta$ p"."   It follows that any well-formed formula of the type C $\delta$ p $\delta$ q, along with substitution and detachment gives you the same power of replacing proper or improper subformulas with other equivalent proper or improper subformulas.
Now, let's suppose that a=b, and b=c.  By the replacement property of equality, in a=b, we can we b by c and obtain a=c.  Thus, the transitive property of equality follows from the replacement property of equality.
Now let's suppose that a=b.  So, we can replace the right b with a obtaining a=a.  Thus, the reflexive property of equality follows from the replacement property.  
Also, under the hypothesis that a=b, since a=a also, we can replace the right "a" in a=a and obtain b=a.  Thus, the symmetrical property of equality follows from replacement.
The upshot comes as that anything which gives us the same power as the replacement property of equality or logical equivalence, gives us the same power as an equational theory with only universal quantifiers.
Therefore, via the law of extensionality, the following axiom set (if all unary functions of orthomodular lattice propositional calculus ensure the following axioms as sound with respect to the semantics of orthomodular propositional logic) has the same power as that of the equational theory, and thus logically should function as an axiom set for the orthomodular lattice propositional calculus.  We might also need something
 commutation of disjunction  1 C δ Aab  δ Aba.

 association of disjunction  2 C δ AAabc δ AaAbc.

 Double negation equivalence 3 C δ NNa δ a.

 A-K absorption              4 C δ AaKab δ a.

 Petrus Hispanus NANaNb-K    5 C δ NANaNb δ Kab.

 Modular Lattice Law         6 C δ Aab δ A[ K (Aab) Nb] b.

 Rule of detachment          {Cαβ, α} ⊢  β.

 The rule of uniform substitution.

We might also need some other axiom(s) which either give us a deduction theorem (such as {CpCqp, CCpCqrCCpqCpr}) or if that doesn't work, then something like CCpqCCqrCpr (if that works).     
The rule of uniform substitution includes substitution for $\delta$.  To know when you can use a substitution for $\delta$ you can do the following:


*

*Assign -1 to the single symbol apostrophe '

*Assign -1 to all lower case letters of the Latin alphabet (or numerically subscripted lower case letters of the Latin alphabet).

*Assign 1 to all binary connectives.

*Assign 0 to all unary connectives.

*Assign 0 to $\delta$.


A uniform substitution for $\delta$ comes as permissible if and only if, it contains at least one apostrophe, when you start with 0 before doing any sums, and form sums from left to right using the above assignments such a summation process never reaches -2, and such a summation process ends with -1.  You could also suppose a "1" in the blank space to the left of the well-formed formula, and consequently, such a summation process will end with 0 and never correspond at any point to -1 if it comes as a permissible substitution.
Some examples of such a summation process:
 C p   '     '

 1 0  (-1) (-2)
 --------------
 C '   z

 1 0 (-1)
 --------------
 A C ' '  δ     '

 1 2 1 0  0   (-1)
 -----------------
 K δ δ ' C p   r

 1 1 1 0 1 0 (-1)

I use the notation where x/ y indicates that x gets substituted with y.  Also, C x- y indicates that we have some well-formed formula which starts with C, has x as its next part, y as its last part, and since we already have x we will detach y.  "*" functions as a separator where the left side of the * and the right side of the "*" come as equiform if you wrote the substitutions indicated out in full.
As an example of a proof I will prove $\vdash$CAAbacAaAbc.
1 C δ Aab  δ Aba.
2 C δ AAabc δ AaAbc.
 1 δ/CA'cAaAbc * 3

3 C CA Aab cAaAbc CA Aba cAaAbc.
 2 δ/' * 4 

4 CAAabcAaAbc.
 3 * C 4 - 5

5 C AAbac AaAbc.
