Negative Translations of Orthomodular Lattices and Their Logic

TL;DR

This paper introduces residuated ortholattices as a new algebraic framework for orthomodular lattices, establishing their properties, logical semantics, and a translation method akin to double-negation translation, with some remarks on decidability.

Contribution

It defines residuated ortholattices, characterizes orthomodular lattices within this framework, and develops a translation method for interpreting orthomodular lattices in residuated ortholattices.

Findings

Residuated ortholattices generalize orthomodular lattices.

Orthomodular lattices are characterized by residual operations.

A translation similar to double-negation is established for interpretation.

Abstract

We introduce residuated ortholattices as a generalization of -- and environment for the investigation of -- orthomodular lattices. We establish a number of basic algebraic facts regarding these structures, characterize orthomodular lattices as those residuated ortholattices whose residual operation is term-definable in the involutive lattice signature, and demonstrate that residuated ortholattices are the equivalent algebraic semantics of an algebraizable propositional logic. We also show that orthomodular lattices may be interpreted in residuated ortholattices via a translation in the spirit of the double-negation translation of Boolean algebras into Heyting algebras, and conclude with some remarks about decidability.