NORMAL IMPLICATIONS, BOUNDED POSETS, AND THE EXISTENCE OF MEETS

J . JAY ZEMAN

The interpretation of certain lattices as logics has long been recognized as a very fruitful exercise; it has aided the gaining of insight into "standard" logics such as the classical and the intuitionist, and has helped open up vistas in the study of "newer" logics such as quantum logic and orthomodular logic in general ([2, 3, 4, 5, 6, 7, 10] are a few examples). As has been argued elsewhere [10], interpretation of a lattice as a logic virtually necessitates the definition of an "implication function" on the lattice. Implication functions so defined can have deep effects on the algebra on which they are defined. Probably the best-known of these effects is expressed in Skolem's proof (see [1], p. 144) that a lattice upon which positive implication (and so a fortiori classical implication) is defined is ipso facto distributive. This effect has been a prime motivation in a fairly extensive body of recent research into the employment of various nonclassical implications (notably modal implications-see [2, 3, 4, 10], for example) in connection with orthomodular logic, which in the general case, of course, must avoid being distributive. The present paper will discuss an effect which a certain large family of implications has on a broad class of partially ordered sets. This will be the class of posets with universal upper and lower bounds (which we shall simply refer to as universally bounded posets, understanding that both bounds are required)-this class includes the orthomodular posets. If we interpret the elements of such a poset as propositions, the universal bounds interpret as universally true and false statements respectively; this class of posets is then of importance in the study of logics.

By "K" we will mean the system so designated by Segerberg [8]. This is the modal logic characterized by the entire class of normal relational frames; it is the most general normal modal system, and was discussed in Zeman [9] under the name "T°". For reference, we note that K may be formulated by adding to the classical PC (expressed lattice-theoretically) the axiom scheme (with L for necessity)

and the rule of inference

As is the case for many modal systems, the pure strict implicational part of K is axiomatizable [11]. The basic result of the present paper will be the following:

This will also apply, of course, to all strict implications of systems containing K; we will call such implications "normal implications." This includes the positive and classical implications, viewed as "degenerate" modal implications. This result has significance in the study of orthomodular logics, since a number of authors have suggested that the more general orthomodular poset rather than the orthomodular lattice be taken as the model of quantum and other orthomodular logics (see, for example, [2, 5, 7]). (I tend to disagree with that approach, since I have great difficulty in coming up with an intuitive interpretation for pairs of propositions for which conjunction (or disjunction) is not defined; such conjunctions may be nonsense in certain cases, but they ought to be able to be written down anyway. Once we leave the realm of lattices, of course, we lose the guarantee of meets and joins for all such pairs, and with it the universal definition of conjunction and disjunction respectively.) Orthomodular posets have universal upper and lower bounds; the definition of any normal implication on an orthomodular poset, then, will force it to be a meet semilattice, and so-since orthomodular posets are also orthocomplemented-a lattice, specifically, an orthomodular lattice. These considerations will provide, I think, a fair amount of input to the "philosophical" dialogue on these systems.

Leaving that dialogue aside for the purposes of this paper, we turn to the strict- implicational part of K. [11] shows that the following two assertions define K-strict implication on a lattice; here É is K-strict:

Rule É2_K will be recognized simply as a rule inserting implication signs on both sides of the sign of deduction, analogous to the rule for L in Gentzenized versions of K (see [9], p 110 ff.). K implication, by the way, may be extended to the system for T's strict implication by adding

which is an assertion we would very naturally associate with an implication operator. This makes Lp ≤ p provable (Lp = 1 É p by definition).

Suppose now that P = áP, ≤ñ is a poset with universal upper and lower bounds; consider a function Ù :P ´ P ® P. At this point we specify that p Ù q for p, q Î P is to be chosen from among the lower bounds of p and q; since the poset has a universal lower bound, the function will be defined for all pairs of elements. We have some freedom in selecting which of the lower bounds of p and q p Ù q will be; the key is to specify p Ù q in such a manner that it will always exist in a universally bounded poset. We would not be free at this point, therefore, to call p Ù q the greatest lower bound of p and q, since such may not exist. We may, however (and it shall be convenient to do so) say that p Ù q is one of the maximal lower bounds of p and q. From this will follow the idempotency of Ù and the fact that 

p Ù 1 = 1 Ù p = p. 

It shall also be convenient to use the following in choosing this lower bound: for each triple p, q, r Î P such that p ≤  q, so choose lower bounds that p Ù r ≤ q Ù r and r Ù p ≤ r Ù q. The lower bounds of p with r will always be a subset of those of q with r; we select from the maximal lower bounds those that "do the job" Ù will then be selected to be isotone on both sides. The following will hold for all p, q, r Î P:

Let us now define K strict implication on P by adding the axioms É0 and É2_K. With 

p = a = b₁ = b₂, 
q = g₁,
r = g₂, 
q Ù r = d, 

(1) -(3) above become the first three premises of É2_K; the conclusion of this application of the rule is:

Clearly, (4) has the effect of making Ù a meet function; if p ≤ q and p ≤  r, then p É q = p É r = 1 by É0, so again by É0, p ≤ q  Ù r, which then is the greatest lower bound of p and q; P is then a meet semilattice.

So that the result may seem less like a rabbit out of a hat, let us quickly run through it with a more familiar appearing implication defined on P; we shall see that for certain formulations of implications we shall require more "care" in . the selection of p Ù q than for K; specifically, we shall make use of the isotone nature of Ù; which was not necessary for our formulation of K-strict. Positive implication is defined on P by the addition of axiom É1 from above, and also:

This is recognized as the familiar deduction theorem. It will hold here as "iff "; with r ≤ p É q, with  É1, and Ù isotone, we get r Ù p ≤ q immediately. Now, we have:

With É1 in the forms p Ù (p É q) ≤  q and p Ù (p É r) ≤  r and Ù isotone, (5) becomes

If p ≤ q and p ≤ r, the left member of this assertion reduces (with idempotency) to p; once again, then, we have p ≤ q Ù r, which is then the meet of q and r.

We note in passing that the above deduction goes through for weaker normal implications formulated in the manner of positive implication; typical is that for S4, which is given by É1 plus:

University of Florida , 
Gainesville, Florida