A natural deduction system for orthomodular logic

TL;DR

This paper introduces a natural deduction system for orthomodular logic, a noncommutative logic related to quantum logic, with semantics aligned to quantum set theory and quantum logic variants.

Contribution

It develops a natural deduction framework for orthomodular logic with physically motivated semantics and extends it to predicate logic systems compatible with quantum theories.

Findings

The deduction theorem holds with Sasaki arrow as implication.

The system is sound for Takeuti's quantum set theory.

The system is sound for a variant of Weaver's quantum logic.

Abstract

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.