  Orthomodular logic is a weakening of quantum logic in the sense of Birkhoff
and von Neumann. Orthomodular logic is shown to be a nonlinear noncommutative
logic. Sequents are given a physically motivated semantics that is consistent
with exactly one semantics for propositional formulas that use negation,
conjunction, and implication. In particular, implication must be interpreted as
the Sasaki arrow, which satisfies the deduction theorem in this logic. As an
application, this deductive system is extended to two systems of predicate
logic: the first is sound for Takeuti's quantum set theory, and the second is
sound for a variant of Weaver's quantum logic.
