TWO BASIC PUREIMPLICATIONAL SYSTEMS
J . JAY ZEMAN
In this paper we shall study two very basic systems of pure implication, and shall show that they are equivalent to the pure implicational parts of certain key modal calculi, namely the systems T° and S4°. These systems are referred to as "key" because of their extreme semantic and syntactic simplicity. T° (equivalent 'to Segerberg's "K" [12]) is the system which is defined by the entire class of normal Kripke or relational frames; that is, it is the system for which no specific assumptions are made about properties of the accessibility relation [9], p. 129 ff. S4° is defined by the set of such frames in which that relation is transitive. The syntactic simplicity is best seen in the fact that Gentzen sequent logics for PC can be extended to either of these systems by the addition of a single appropriate simple rule (see [9], p. 125, p.198). The basic nature of these implications gives promise of their profitable employment in the study of orthomodular logic, including the socalled quantum logic (a few general examples of the literature in the area of this kind of logic are [1, 3, 4, 5], ch. 5, 7, 10); this is a field of potential importance both philosophically and mathematically. As discussed in [10], classical (and even positive) implication will not do for the general orthomodular logic, since definition of positive implication on an orthomodular lattice automatically renders it distributive and so Boolean. However, as noted in [10], certain nonclassical implications can be defined on an orthomodular lattice without rendering it Boolean. Notable among these are certain modal implications; the pinning down of these basic modal implications may then be considered a potential advance in the theory of orthomodular logic. In addition to their potential applicability in the area of orthomodular logic, these systems have received philosophical application in the study of the theory of inquiry of C . S. Peirce [8].
In what follows, we shall use the standard implication sign 'C' as the sign of T° or S4° strict implication. When it is necessary to distinguish the modal implications from classical or positive implication, we shall use the sign 'F' for the latter two. The letters p, q, r, etc. will be used mechanically as they are when dealing with systems with a postulated rule of substitution (as with those of [9]); formally, however, we shall think of them as schema letters, and so avoid the use of a postulated rule of substitution; axioms, then will be stated by means of axiomschemata.
A key feature in these systems will be a rule of Cintroduction, or CI. This rule governs the generation of certain sequents, or "deducibility claims"; it permits us to infer from the set of n + 1 sequents:
a b_{1} 
a, g_{1} b_{2} 
. 
. 
. 
a, g_{1} , . . . , g_{n1} b_{n} 
a, g_{1} , . . . , g_{n} d 
to the sequent:
Cb_{1}g_{1}, . . ., Cb_{n}g_{n} Cad
We note that the (i + 1)th sequent in the above set (i £ n) differs from the ith in having g_{i} added to its antecedent and in having b_{(i + 1)} as its succedent.
The prooftheoretic systems of this paper will make use of this rule.
A "Hilbertstyle" axiomatization of pureimplicational T° will be called IT° and will consist of CI plus the axiom schema:
C1  CpCqq 
plus the following recursive definition of '':
We write G q and say "q is deducible from the set (possibly empty) of formulas G" iff there is a list of formulas (the deduction) ending with q and each member of which is either:
Note that in c above, detachment is restricted. As we shall see later, permitting Cab to be any previous formula in the deduction, rather than a theorem only, extends the system to the pure strict implicational part of T°.
We may extend IT° to the system I4°, which we will show to be the pure strict implicational part of S4°, by adding to it the axiom schemata:
C2  CCpqCCqrCpr  
C3  CCqrCCpqCpr 
These systems may also be stated as Gentzenstyle sequentlogics.
Here we would have rule CI (replacing '' by '®' to distinguish the formulations), and instead of axiom schema C1 and the above definition of deduction, we would have the sequent axiom schema a ® a And the rules of weakening and contraction. This system may be called LIT°; LI4° may be formulated by adding the rule
a, G ® b  

®C  provided all members of G are strict  
G ® Cab 
to LIT°.
Kripkestyle semantics for these systems are very easily set down; The rules employed are as follows (techniques are patterned after [9]):
Cr:  If Cab occurs on the right side of a semantic tableau t, begin a new tableau auxiliary to t and having a on its left and b on its right. 

Cl:  (a) 
If Cab occurs on the left of a tableau t and there are tableaux auxiliary to t, split each of those auxiliary tableaux (auxtabs) writing a on the right of one of the tableaux resulting from the split and b on the left of the other. 
(b) 
If Cab occurs on the left of a tableau t, write Cab on the left of every tableau auxiliary to t. 
Semantics for IT° is given by Cr and Cl(a); for I4°, clause (b) of Cl is included as well. We note that S4° is the system defined by the class of Kripke frames in which the accesibility relation is transitive; carrying strict implications into auxtabs (in addition to splitting as in Cl(a)) will effectively reflect this transitivity.
The above formulations all have primitive Cstrict as their only connective. We shall require also standard formulations of T° and S4° with L (necessity) and material implication primitive; these will be used as tools in the study of the strict implicational systems. As we have noted, we shall use F as the sign of material implication. Since we are interested in strict implication, we shall be concerned with the FL fragments of, specifically, Gentzenstyle sequentlogics for T° and S4°, which will be called, respectively, LT° and LS4°. By methods which must be considered wellknown, cut elimination is provable for both systems as they will be stated, so to get the complete FL fragments of T° and S4°, we need only the structural rules plus the rules for F and L. We are, in fact, not interested in the entire FL fragments of these systems, but in the subsets of these fragments in which F and L always occur only in the combination LF; this is the strict implicational part with defined strict implication; we may call it the "LFpure" part of LT° and LS4° respectively.
It will be noted in the rules as we shall state then that the F rules as well as those for L are given with singular succedent. This means, of course, that the F part of this system is positive rather than classical implication. There is no problem here, however, for F's will be placed in sequents of this system only where strict implications can be placed in sequents of LT° and LS4°. The strict implicational parts of all modal systems contained in S4 are contained in positive implication, so having positive implication rules for F will be enough. The rules then are:





LT°'s FL fragment is given by the structural and implication rules plus LI; LS4° has ®L in addition. Notation and terminology are those of [9]; the formulation of LS4° given here differs slightly from that of [9], but is clearly equivalent.
A lemma concerning positive implication As a part of our study of IT° and I4°, we will wish to establish a lemma about positive implicational sequent logic; the rules will be the structural rules and the above rules for F. Suppose that we have a sequent whose antecedent is n £ 0 implications, and whose succedent is also an implication. Suppose further that this sequent is provable given sequent logic for positive implication, and that at some point in the proof each of the n + 1 F's has been introduced by a logical rule (rather than being introduced entirely by weakening). What we wish to establish is that this all is the case iff indices 1, . . ., n are assignable to the sequent's antecedent formulas making it
(1)  Fb_{1}g_{1}, . . ., Fb_{n}g_{n} ® Fad 
and such that the following set X of sequents are all provable:
a ® b_{1} 
a, g_{1} ® b_{2} 
. 
. 
. 
a, g_{1} , . . . , g_{n1} ® b_{n} 
a, g_{1} , . . . , g_{n} ® d 
The relationship of this lemma to rule CI of IT° should be clear.
The "if" portion of this proof is elementary; given the n + 1 sequents above and the two rules for F, it is a simple matter to prove (1), and so the sequent in question. The proof in the other direction is a bit more involved.
Since the normal form theorem holds for this system, we see that by ®F, with (1) holding, then also
(2)  a, Fb_{1}g_{1}, . . ., Fb_{n}g_{n} ® d 
must be provable. This sequent, in turn, must be able to result from at least n applications of F® beginning from an appropriate number of premises; each of these premises is formed by 0 or. more weakenings on a provable sequent each of whose formulas is drawn only from a, d, and the n each b and g. As an example, we offer the following derivation of the sequent Fpq, Fqr ® Fpr:
q ® q  r ® r  



p ® p  q, p ® q  r, q, p ® r  



p, Fqr ® p  q, p, Fqr ® r  







In the above endsequent take the occurrences of p, q, and r as follows, reading from left to right: p = b_{1}, q = g_{1}, q = b_{2}, r = g_{2}, p = a, r = d. It will be seen that the initial premises are indeed as suggested, and that the provable sequents p ® p; q, p ® q; r, q, p ® r are the set of n + 1 (here three) sequents which this lemma holds to be provable iff the endsequent is.
We turn now to the lemma in general. Suppose, first of all, that in sequent (2) n = 0. (2) then is a ® d, which is itself the sole member of set X for this case. Now suppose that whenever n = k, the lemma holds for sequents in form (2) . Consider the case in which n = k + 1. By the invertibility of F® with itself [9], p.52 the proof of (2) may be arranged to conclude as follows:




g_{n}, a, Fb_{1}g_{1}, . . ., Fb_{k}g_{k}, Fb_{n}g_{n} ® d 
The left premise of this application of F® is of form (2) with k implications in its antecedent; it then falls under the scope of the induction hypothesis, and so the set of sequents:
a ® b_{1} 
a, g_{1} ® b_{2} 
. 
. 
. 
a, g_{1} , . . . , g_{n1} ® b_{n} 
a, g_{1} , . . . , g_{n} ® d 
is provable. But this is precisely the first n members of the set X for a sequent in form (2) with n = k + 1. Now look at the right premise of this rule application; it has g_{n} replacing the Fb_{n}g_{n} of the endsequent. It should be clear that if we climb higher and higher in the tree proof keeping always as far right as possible (always climbing via the right premise) we shall successively replace implications Fb_{i}g_{i} with g_{i}. Climbing n such steps will give us the sequent a, g_{1} , . . . , g_{n} ® d which is the (n + 1)th member of the set X for this case. The lemma then stands proven.
We note that in the proof there may be cases in which a, g_{1} , . . . , g_{i} ® b_{j} for i < j  1 (an example is the premise q ® q ;in the earlier setdown derivation). Clearly, this causes no difficulty, as the premise may be converted by weakening into exactly the jth member of X.
The completeness of IT° We shall now establish that G q holds for IT° iff G ® q is an LT° theorem. It is understood, of course, that the formulas in these sequents are Cpure, with C in LT° defined as LF. The "only if" direction of this metatheorem is quite easy to establish;  LFpLFqq is easily established in LT°, as is the form of detachment for IT° (as usual, with the aid of cut, which is itself eliminable in LT°). A little inspection and reflection on the previous section will show that given the n + 1 sequents which count as premises for IT°'s rule CI, one can easily prove in LT° a sequent in the form of the conclusion of CI; all IT° provable sequents are then provable in LT°.
We now will show that all LFpure sequents which are LT° provable are also IT° provable, taking C instead of LF everywhere. We do this by induction on the number of applications of rule LI in relevant LT° proofs. Suppose that there have been no applications of this rule in the proof of G ® q. Then there could have been no applications of the rules for F either, since the sequent is to be LFpure. The proof then cannot have involved the logical rules, and q must be among the G,. But then G q holds for IT°.
Suppose now that whenever the number of applications of LI is £ k in a relevant LT° proof, this metatheorem holds. Consider a proof with k + 1 such applications. This proof will end as follows:
Fb_{1}g_{1}, . . ., Fb_{n}g_{n} ® Fad 



LFb_{1}g_{1}, . . ., LFb_{n}g_{n} ® LFad 
All the b_{i} and g_{i} as well as a and d must be LFpure for the endsequent to be so. We may ignore cases in which some of the Fb_{i}g_{i} are inserted solely by weakenings, for as we shall see, there is an analog of weakening provable for IT°, and so weakenings may be duplicated there. But this makes the premise of (3) a sequent in the form of (1) of the previous section, which means that by the lemma of that section, the indices 1, . . ., n may be assigned to the formulas of that premise so that the sequents
a ® b_{1} 
a, g_{1} ® b_{2} 
. 
. 
. 
a, g_{1} , . . . , g_{n1} ® b_{n} 
a, g_{1} , . . . , g_{n} ® d 
are all LT° provable. But these sequents are all provable in k or fewer applications of LI, and are LFpure; by the induction hypothesis, then, with '' replacing '®' they are all provable for IT°. But they are precisely the premise sequents for rule CI, and so
(4)  Cb_{1}g_{1}, . . ., Cb_{n}g_{n} ® Cad 
is provable for IT°, as required.
We earlier indicated that we must show that an analog of weakening holds for IT°; this is not completely trivial; it might be expected that whenever a deduction G ® J holds in IT° then h, G ® J also must hold; the cases in which J is generated by clause (a), (b), or (c) of the definition of deducibility clearly cause no problem; when G ® J holds by clause (d), however  that is to say when it is the result of an application of rule CI  we must show the proof explicitly.
SupposeG ® J is a result of CI; it then is in form (4), with '' for '®' . Consider the set of the n + 1 premises of the CI application; extend this set by adding a a ® a as an additional premise, and reiterate a in the antecedents of each of the members of the original set of premises (induction here is on length of deduction; the premises of the CI will fall in the scope of the induction hypothesis, and so may be weakened in this manner). If CI is applied to the new set of premises, we get:
(5)  Caa, Cb_{1}g_{1}, . . ., Cb_{n}g_{n} Cad 
By axiom C1, we have ChCaa; given h as a step in a deduction, then, we can get Caa there, and so if (5) holds, so too does
(6)  h, Cb_{1}g_{1}, . . ., Cb_{n}g_{n} Cad 
We then have our analog of weakening for this case, as required.
We have noted that removing the restriction on clause (c) of the definition of deduction in IT° is sufficient to extend this system to T's pure strict implicational part; without the restriction, the sequent
(7)  p, Cpq q 
is immediately provable (compare Lewis and Langford's axiom B7 of [6], p. 493, which is deductively equivalent there to CLpp). Using (7) and p p as premises for CI, we get
(8)  CpCpq Cpq 
One more application of CI gives us CCpCpqCpq, Hilbert's law, which is one of the axioms of the formulation of [11], p. 67 for T's pure strict implicational part. The other axioms and rules of that formulation are provable in elementary fashion (the infinite set of rules of Hacking's III is provable making use of the fact that all pure strict implicational sequents of T are provable in proofs with the subformula property; axiom (3) of that formulation is provable by CI, using Cqr, Cpq Cpr, and Cqr Cqr as premises).
Pure implicational S4° The system I4° results from the addition of axiom schemata
C2. CCpgCCqrCpr
C3. CCqrCCpqCpr
to IT°. As we earlier noted, the addition of the rule ®L of S4 sequent logic to the system LT° results effectively in LS4°, the sequent logic for S4°. As with LT°, cut elimination is provable, so all provable sequents are provable in proofs with the subformula property, and so all provable LFpure LS4° sequents will be provable with the F and L rules as the only logical rules. To show, then, that I4° is the pure strict implicational part of S4°, we must prove for I4° an analog of LS4°'s rule ®L. For the LFpure part of LS4°, this rule will always be used immediately after an application of ®F; the I4° analog, then, will be the S4 version of the deduction theorem, with the definition of deduction as earlier stated in this paper. We must show, then, that given I4° we can establish:
(DT) If a, G b, then G Cab, provided all the G are strict.
Induction is on the length of the deduction of b from a, G cases are as indicated in the definition of deduction:
(a)i: b may be the same as a; DT then holds by provability of Cbb.
(a)ii: b may be one of the G. Take axiom C1 with q for r; this then is
(9)  CCpqCCqqCpq 
Semisubstitutivity of implication holds in IT^{°} (and indeed, in the stronger form in I4^{°}, with C2, C3, and Cpp provable, see [9], pp. 98, 1623). With axiom schema C1, then, we may replace the Cqq in (9) by r, getting
(10)  CCpqCrCpq 
Since b is one of the G, it is strict, and so can enter into a detachment with (10); from G b then, we get G Crb; with r as a, we have DT for this case.
(b) b may be an axiom. All axioms, of course, are strict, and so we use (10) as above to get G (or any set of formulas) yielding Cab.
(c) b may result from a detachment involving a theorem Cgb and a previous line g of the deduction. Cgb and axiom schema C3 give us:
(11)  CCpgCpb 
By the induction hypothesis, G Cag. This with the theorem (11) gives us (within the restriction on detachment) G Cab.
(d) a, G b may result from an application of rule CI. In this case, it is
(12)  Cb_{1}g_{1 },. . ., Cb_{i}g_{i} , . . ., Cb_{n}g_{n} Czd 
1 £ i £ n, with Cb_{i}g_{i} the a of DT, and Czd the b. The set of sequents
Cb_{i}g_{i } Cb_{i}g_{i}  
Cb_{i}g_{i, }Cb_{1}g_{1 } Cb_{i}g_{i}  
.  
.  
.  
Cb_{i}g_{i, }Cb_{1}g_{1 }, . . ., , . . ., Cb_{(}_{n1)}g_{(}_{n1)} Cb_{i}g_{i} 
all hold for I4^{°}. This set plus sequent (11) is a set of premises for another application of CI; the result of this will be:
(13)  CCb_{i}g_{i}Cb_{1}g_{1 }, . . ., Cb_{i}g_{i} , . . ., CCb_{i}g_{i}Cb_{n}g_{n} CCb_{i}g_{i}Czd 
Our intention in the above set of sequents is that each antecedent contain Cb_{i}g_{i} only in the displayed position; the Cb_{i}g_{i} of (12) the set's antecedent is the a of CI; the antecedent of (13) then lacks CCb_{i}g_{i}Cb_{i}g_{i}. By (10), the formuila Cb_{j}g_{j} will give us, in each case, C Cb_{i}g_{i} Cb_{j}j_{j}. We can then get from the antecedent of (12) less Cb_{i}g_{i} whatever we get from the antecedent of (13); we then have
(14)  Cb_{1}g_{1 }, . . ., Cb_{n}g_{n} CCb_{i}g_{i} Czd  
(less Cb_{i}g_{i}) 
But (14) is G Cab for this case, as required; DT then holds. Proof of axioms C2 and C3 given IT^{°} and DT is elementary; we then have I4^{°} as the pure strict implicational part of S4^{°}.
Semantics for IT^{°} and I4^{°} As earlier mentioned, Kripkestyle semantics for IT^{°} are given by the rules C r and C1(a) for semantic tableaux. Semantics of this kind are available for the whole system T^{o} [9], p. 129 ff. Rules for T^{°} in addition to those for the PC are:
Lr: Where La occurs right in a tableau, begin a new auxtab having a on its right.
L1: Where La occurs left in a tableau, write a on the left of every tableau auxiliary to that one.
We will again be interested in the LFpure part of T^{°}; the PC tableau rules for F are:
Fr: Where Fab occurs right in a tableau, write a left and b right in that tableau.
F1: Where Fab occurs left in a tableau, split that tableau writing a on the right of one of the resulting tableaux and b on the left of the other.
We wish to show that a tableau construction begun with Cpure formulas closes given the IT^{°} rules iff the construction begun with the same formulas, taking C as LF, closes given the T^{°} rules.
The induction is on the number of Cr applied, in the "onlyif" direction; and is on the number of Lr applied, in the "if" direction of the proof. Suppose the number of Cr (Lr) applied in getting a closing tableau is zero; then no C1 can have been applied because application of Cr is the only way to get an auxtab (no L1 can have been applied because application of Lr is the only way to get an auxtab, and no F rules could have been applied for the initial formulas in the tableau are LFpure). Thus, if no Cr (Lr) has been applied and the tableau construction closes, some initial formula on the right of the IT^{°} (T^{°}) tableau must be the same as some on the left; this condition will also cause the analogous T^{°} (IT^{°}) tableau to close.
Suppose that when (with C = LF) a tableau construction for IT^{°} (T^{°}) closes employing no more than k applications of Cr (Lr) the T^{°} (IT^{°}) tableau construction begun with the same formulas also closes. The IT^{°} and T^{°} constructions then begin:
G  Q  
Cb_{1}g_{1}, . . .,Cb_{n}g_{n}  Cad  
¯
a  d  
etc.
and (for T^{°})
G  Q  
LFb_{1}g_{1}, . . .,LFb_{n}g_{n}  LFad  
¯
Fb_{1}g_{1}, . . .,Fb_{n}g_{n}  Fad  
X    X  
a  d  
etc.
The constructions are clearly the same below "etc." Suppose the IT^{°} construction closes. Then its auxtab closes. By the induction hypothesis, a T^{°} tableau beginning with a left and d right then must also close, and so the T^{°} auxtab and so the whole construction closes, establishing the "only if" part of the proof.
Suppose now that the T^{°} construction closes. Since an application of Ll is required for this, none of the formulas on the left is the same as any on the right of the main tableau, and so Fad differs from each of the n implications shown on the left of the auxtab. Further, since the a and d as well as each of the b_{i }and g_{i}, 1 £ i £ n, are all LFpure, none of the implications beginning with an F can enter into a "closing" with any of the formulas below line XX. Since the construction closes, then, a T^{°} tableau beginning with the formulas which will be below XX of the F1 are done must close. But then so must, by the induction hypothesis, an IT^{°} tableau beginning with the same formulas; such a tableau is precisely the auxtab of the corresponding IT^{°} construction. That construction then closes, completing the proof.
An argument from a set of formulas r to a formula a is valid iff the tableau construction begun with r left and a right closes, for either system. Given what has proceded in this paper, then, it is easy to see that if such an argument is IT^{°} valid, then r f a holds for the prooftheoretic IT^{°}, giving us a semantic completeness result.
The result is easily extended to I4° if we note that [9]'s rule for Lleft in S4^{°} reflects the transitivity of the accessibility relation precisely in the manner that clause (b) of our C1 does, by iterating necessary statements on the left side of tableaux into the left side of auxtabs.