STRICT IMPLICATION IN A SEQUENCE OF EXTENSIONS O F S4 by DOLPH ULRICH in West Lafayette, Indiana (U.S.A.) l) ( A l ) C p p , (-42) CCpqcrCpq, (A3) CCpCqrCCpyCpr,
and as sole rule of inference detachment ("from N and Cq3 infer 8"). Standard terms concerning axiomatic systems (theorem, deductive consequence, and the like) will be employed, with normal supporting notation, in the ordinary way and so without individual explanation.
A system L' whose only rule is detachment is an extension of a similar system L provided its set of theorems is closed under substitution and includes the theoremsof the latter. For extensions of C4, we have available the well-known L e m m a 1 (Deduction theorem for extensions of C4). Let L be any extension of C4 and let W be any set of strict wffs. Then for all wffs 01 and tf? in S, if W, N kI,p then
The straightforward proof may be found, for example, in [l], and so is not repeated. Defining an L-theory to be any set of wffs containing the theorems of L and closed under detachment, hence, under deductive consequences in L, we assure ourselves also of w t 1, cap. l) Some of the results presented here were announced, albeit with more complicated constructions and unnecessarily intricate proofs, in [14] and [15]. I owe general thanks to J. MICHAEL DUNN, with whom a number of these resultg have been discussed over the years. I am indebted also to the members of my Spring 1973 seminar, Mssrs. HADDEN, LYMAN, PARKER, PAVLOVIC and, especially, RALPH MOON. The latter's skill and enthusiasm, through our continuing discussions, have greatly improved the presentation. Lemma 2. Let W be a n L-theory, L any extension of C4. Then for all (x, p in S , Cap E W only if oc 4 W or p E W.
L is to be the set of all L-theories. S is clearly the strongest member of L ; let TL be the weakest, that is, the set of theorems of L.
By a frame we shall mean, as usual, a pair ( W, R ) with W a nonempty set and R a binary relation in W. An assignment in such a frame is a function U from ( p , q, r, . . .> x W into (T, F). Each assignment U can be extended uniquely to a function V from S x W into (T, F) in such a way that for oc, /? in S and W in W, V(Coc/?,w) = T if and only if V(oc, W') = F or V(p, W') = T whenever WRW'. In this caae, we call V an impliicational valuation and ( W, R, V } an implicational model. We'll say the model is "reflexive", "transitive" and so on when R is; and of course a wff (x is valid in the model just in case V(oc, W) = T for each W in W.