Alternative formulations include propositions derivable via a natural deduction, sequent calculus or tableaux system. Despite the relatively developed proof theory, quantum logic is not known to be decidable.