A common method of obtaining the classical modal logics, for example the Feys system T, the Lewis systems, the Brouwerian system etc., is to build on a basis for the propositional calculus by adjoining a new symbol L, specifying new axioms involving L and the symbols in the basis for PC, and imposing one or more additional transformation rules. In the jargon of algebraic logic, which is the point of view we shall adopt, the “necessity” symbol L may be interpreted as an operator on the Boolean algebra of propositions of PC. For example, the Lewis system S4 may be regarded as a Boolean algebra ℒ together with an operator L on ℒ having the properties: (1)Lp ≤ p for all p in ℒ, (2)L1 = 1, (3) L(p → q) ≤ Lp → Lq for all p, q in ℒ, and (4) Lp = L(Lp) for all p in ℒ. Here, of course, → denotes the material implication connective: p→q = p′ ∨ q. It is easy to verify that property (3) may be replaced by either (3′) L(p ∧ q) = Lp ∧ Lq for all p, q in ℒ, or by (3″) L(p → q) ∧ Lp ≤ Lq for all p, q in ℒ. In particular, it follows from (1) through (4) above that L is a decreasing, idempotent and isotone operator on ℒ. Such mappings are often called interior operators.In a previous paper [5], we considered the problem of introducing an implication connective into a quantum logic. This is greatly complicated by the fact that the quantal propositions band together to form an orthocomplemented lattice which is only “locally” distributive. Such lattices are called orthomodular. For definitions and further discussion, the reader is referred to that paper. In it, we argued that the Sasaki implication connective ⊃ defined by p ⊃ q = p′ ∨ (p ∧ q) is a natural generalization of material implication when the lattice of propositions is ortho-modular. Indeed, if unrestricted distributivity were permitted, p ⊃ q would reduce to the classical material implication p → q. For this reason, we choose ⊃ to play the role of material implication in an orthomodular lattice. Further properties of ⊃ are enumerated in Example 2.2(1) and Corollary 2.4 below.
Algebraic Approach to Algorithmic Logic
