TWO BASIC PURE-IMPLICATIONAL 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 so-called 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 non-classical 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 axiom-schemata.

A key feature in these systems will be a rule of C-introduction, 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 b1

a, g1 b2

.

.

.

a, g1 , . . . , gn-1 bn

a, g1 , . . . , gn d

to the sequent:

Cb₁g₁, . . ., Cb_ng_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 proof-theoretic systems of this paper will make use of this rule.

A "Hilbert-style" axiomatization of pure-implicational T° will be called IT° and will consist of CI plus the axiom schema:

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:

1. One of the G, or 
2. An axiom, or 
3. Of form b when Cab and a is a previous line of the deduction, or 
4. G θ is derived by rule CI.

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:

These systems may also be stated as Gentzen-style sequent-logics.

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

to LIT°.

Kripke-style semantics for these systems are very easily set down; The rules employed are as follows (techniques are patterned after [9]):

Semantics for IT° is given by C-r and C-l(a); for I4°, clause (b) of C-l 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 C-l(a)) will effectively reflect this transitivity.

The above formulations all have primitive C-strict 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 F-L fragments of, specifically, Gentzen-style sequent-logics for T° and S4°, which will be called, respectively, LT° and LS4°. By methods which must be considered well-known, cut elimination is provable for both systems as they will be stated, so to get the complete F-L 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 F-L 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 "LF-pure" 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 F-L 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

and such that the following set X of sequents are all provable:

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

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:

In the above endsequent take the occurrences of p, q, and r as follows, reading from left to right: p = b₁, q = g₁, q = b₂, r = g₂, 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:

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:

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_ng_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_ig_i with g_i. Climbing n such steps will give us the sequent a, g₁ , . . . , 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₁ , . . . , g_i ® b_j for i < j - 1 (an example is the premise q ® q ;in the earlier set-down 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 C-pure, 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 LF-pure 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 LF-pure. 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:

All the b_i and g_i as well as a and d must be LF-pure for the endsequent to be so. We may ignore cases in which some of the Fb_ig_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

are all LT° provable. But these sequents are all provable in k or fewer applications of LI, and are LF-pure; 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

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, Cb1g1, . . ., Cbngn 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, Cb1g1, . . ., Cbngn 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 LF-pure 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 LF-pure 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

Semisubstitutivity of implication holds in IT^° (and indeed, in the stronger form in I4^°, with C2, C3, and Cpp provable, see [9], pp. 98, 162-3). With axiom schema C1, then, we may replace the Cqq in (9) by r, getting

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)

Cb1g1 ,. . ., Cbigi , . . ., Cbngn Czd

1 £ i £ n, with Cb_ig_i the a of DT, and Czd the b. The set of sequents 

		Cbigi  Cbigi
		Cbigi, Cb1g1 Cbigi
		.
		.
		.
		Cbigi, Cb1g1 , . . .,  , . . ., Cb(n-1)g(n-1) Cbigi

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)

CCbigiCb1g1 , . . ., Cbigi , . . ., CCbigiCbngn CCbigiCzd

Our intention in the above set of sequents is that each antecedent contain Cb_ig_i only in the displayed position; the Cb_ig_i of (12) the set's antecedent is the a of CI; the antecedent of (13) then lacks CCb_ig_iCb_ig_i. By (10), the formuila Cb_jg_j will give us, in each case, C Cb_ig_i Cb_jj_j. We can then get from the antecedent of (12) less Cb_ig_i whatever we get from the antecedent of (13); we then have

(14)		Cb1g1 , . . ., Cbngn CCbigi Czd
		(less Cbigi)

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, Kripke-style semantics for IT^° are given by the rules C- r and C-1(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:

L-r: Where La occurs right in a tableau, begin a new auxtab having a on its right.

L-1: 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 LF-pure part of T^°; the PC tableau rules for F are:

F-r: Where Fab occurs right in a tableau, write a left and b right in that tableau.

F-1: 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 C-pure 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 C-r applied, in the "only-if" direction; and is on the number of L-r applied, in the "if" direction of the proof. Suppose the number of C-r (L-r) applied in getting a closing tableau is zero; then no C-1 can have been applied because application of C-r is the only way to get an auxtab (no L-1 can have been applied because application of L-r is the only way to get an auxtab, and no F rules could have been applied for the initial formulas in the tableau are LF-pure). Thus, if no C-r (L-r) 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 C-r (L-r) the T^° (IT^°) tableau construction begun with the same formulas also closes. The IT^° and T^° constructions then begin:

¯

etc.

and (for T^°)

¯

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 L-l 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 LF-pure, none of the implications beginning with an F can enter into a "closing" with any of the formulas below line X-X. Since the construction closes, then, a T^° tableau beginning with the formulas which will be below X-X of the F-1 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 proof-theoretic IT^°, giving us a semantic completeness result.

The result is easily extended to I4° if we note that [9]'s rule for L-left in S4^° reflects the transitivity of the accessibility relation precisely in the manner that clause (b) of our C-1 does, by iterating necessary statements on the left side of tableaux into the left side of auxtabs.