"And then"

"And Then"

1. In an earlier paper¹ I have treated the formal logic of the temporal connective »and next». Use of this connective presupposes that time is a discrete medium, a linear ordering of occasions (moments, time-points) which proceeds from one occasion to the next, from this to the following next, and so forth.
   The logic of this connective was presented in the form of an axiomatized calculus. The calculus had the following vocabulary:
a.   Variables p , q , r , . . .  .
b.   Truth-connectives ~, &, v, →, and ↔.
c.   A binary connective T (»and next»).
d.   Brackets.
   The well-formed formulae of the calculus, the T-expressions, we define as follows:
a.   A variable is a T-expression.
b.   A molecular compound of T-expressions is a T-expression. (For the purpose     of forming molecular compounds, the connective T functions in the same     way as the other binary connectives of the calculus, viz. v, &, →, and ↔.)
In order to save brackets we adopt the following convention concern­ing the »binding force» of the connectives: ~ is the weakest, and then follow in order of increasing strength &, v, →, ↔ and T . By virtue of this convention we can, e.g., for ((((~p & q) vr) → s) ↔ u) Tw write simply ~p & qvr → s ↔ uTw.

The axioms of the calculus were²:
A0. A set of axioms of (»classical», two-valued) Propositional Logic (PL).   
Al. (pvqTrvs) ↔ (pTr) v (pTs) v (qTr) v (qTs).
A2. (pTq) & (rTs) ↔ (p & rTq & s).
A3.  p ↔ (pTqv~q).
A4. ~(pTq & ~q).
   The rules of inference of the calculus are the usual rules of substitution and detachment, and a Rule of Extensionality to the effect that provably equivalent T-expressions are interchangeable salva veritate.
    By the universe of a given T-expression we understand the set of vari­ables p, q,... which appear in it. By the width of the universe we mean the number of variables in the set.
   By a history we understand a T-expression of the form — T(— T (— T (...T —)))..., where each occurrence of »—» represents an occurrence of a state-description in a given universe of (some n) variables p, q,... . (The first sequence of dots in the history indicates an arbitrary number of repetitions of the pattern T(— , and the second sequence indicates as many closing brackets as the first sequence indicates repetitions of the pattern.) By the length of a history we understand the number of success­ive state-descriptions in it. The total number of possible histories of length m in a universe of width n is 2^mn.
It may be shown that every T-expression is provably equivalent with a disjunction of histories (of equal length) in the universe of the expres­sion. This disjunction will be called the T-normal form of the T-expression.
   The notion of a history provides us with a means of defining the notion of logical truth for our calculus. Consider a T-expression which is the dis­junction of all the possible histories of length m in its own universe. This expression says that, from a first moment to an m:th, the world develops in either this or this or ... or this of 2^mn different ways (enume­rating them all). Then, what the expression says is a »mere tautology». For it only says that the world will develop in some possible way without restricting the possibilities. We shall call such an expression a T.-tautology.
   The definition of logical truth gives us a criterion of (semantic) completeness of our calculus. The calculus is complete, if and only if,

i. every T-tautology is a T-theorem, and
ii. the T-normal form of every T-theorem is a T-tautology.

It may be shown that the calculus of the connective »and next» is, in the sense defined, semantically complete.
2. In the present paper I shall develop a logic of' the connective »and then». Use of this connective does not presuppose that time is discrete,

that there exists a next moment. Nor does it presuppose that time is dense or continuous. The normal use of »and then» is compatible with all three possibilities as regards the nature of the time-medium. To say that it is the case that p and then q is to say that it now is the case that p and at some later time will be the case that q.
   The logic of this connective too will be presented in the form of an axiomatized formal calculus. The vocabulary of the calculus for »and then», like that of the calculus for »and next», is the vocabulary of PL enriched with a symbol for a new binary connective. For the sake of convenience, we shall symbolize this new connective (»and then»), too, with the letter T. The definition of the expressions (well-formed formulae) of the calculus then remains unchanged.
It is obvious that the axioms A1, A3, and A4 remain valid, if the symbol T is read »and then». So these axioms and, of course, A0 can be taken over unchanged into the new calculus.
    It is also obvious that A2 is not (generally) valid, when T is read »and then». The fact that at some later time it will be the case that q and also that at some later time it will be the case that s does not entail that at some later time it will be the case that both q and s. The two may come true simultaneously. But it is also possible that the one comes true first and then the other. So there are three possibilities in all. Their symbolic expressions are »q & s», »qTs» and »sTq» .If we replace the expression »q & s» in A2 by »q & s v (qTs) v (sTq)», then what the axiom says is true for »and then». This is the only modification in the axioms which we need.³ In order to distinguish the axioms for »and next» from the axioms for »and then» I shall call the latter set B0–B4. The axioms for »and then» are thus:
B0. A set of axioms of PL.
B1. (pvqTrvs) ↔ (pTr) v (pTs) v (qTr) v (qTs).
B2. (pTq) & (rTs) ↔ (p & rTq & s v (qTs) v (sTq)).
B3. p ↔ (pTqv~q).
B4. ~(pTq & ~q).
    The rules of inference remain unchanged.
    3. We next prove some theorems of the new calculus. Some of them are identical with theorems for the connective »and next» and proved in the same way. Others are identical, but require a different proof.

(1) pv~p. PL.
(2) (pTqv~q) v (~pTqv~q). From (1) by Rule of Extensionality.
T1.  (pTq) v (pT~q) v (~pTq) v (~pT~q). From (2) by B1.
Substituting p for q in T1 we immediately obtain as a corollary
T2.  (pTp) v (pT~p) v (~pTp) v (~pT~p).
(1) (pTq) v (pT~q) ↔ (pTqv~q). From B1.
(2) (pTq) v (pT~q)→ p. From (1) by B3 and PL.
T3.  (pTq) → p. From (2) by PL.
(1)  (p & ~pTq) → p & ~p. From T3 by Substitution.
(2)  ~(p & ~p). PL.
T4.  ~(p & ~pTq). From (2) and (1) by PL and Detachment.
(1) p & (qTr) ↔ p & (p & q v ~p & qTr). Extensionality.
(2) p & (p & q v ~p & qTr) ↔ p & (p & qTr) v p & (~p & qTr). From (1) by B1 and PL.
(3) p & (~p & qTr) → p & ~p. From T3 and PL.
(4) ~(p & ~p). PL.
(5) ~(p & (~p & qTr)). From (3) and (4) by PL.
(6) p & (p & qTr) v p & (~p & qTr) ↔ p & (p & qTr). From (2) and (5) by PL.
(7) (p & qTr) → p. From T3 (by PL).
(8) p & (p & qTr) ↔ (p & qTr). From (7) by PL.
T5.  p & (qTr) ↔ (p & qTr). From (1), (2), (6), and (8) by PL.
    Let t be an arbitrary tautology of PL, for example pv~p.
(1)  p & (tTq) ↔ (p & tTq). From T5.
(2)  p & t ↔ p. PL.
T6.  (pTq) ↔ p & (tTq). From (1) and (2) by Rule of Extensionality.         
T7.  (p & qTr) → (pTr). Immediately from T5 by PL.
(1)  (pTq) ↔ (pTq & rvq & ~r). Extensionality.
(2)  (pTq & rvq & ~r) ↔ (pTq & r) v (pTq & ~r). B1.
T8.  (pTq & r) → (pTq). From (2) and (1) by PL.
(1)  (pTq) & (pTr) ↔ ((pTq) & pTr). From T5.
(2)  ((pTq) & p) ↔ (pTq). From T3 by PL.
T9 (pTq) & (pTr) ↔ ((pTq)Tr). From (2) and (I) by Extensionality.        
(1)  (pTq) & (pTr )↔ ((pTr)Tq). From T9 by Substitution.
T10. ((pTq)Tr) ↔ ((pTr)Tq). From (1) and T9 by PL.
(1)  (pTq) & (pTr) ↔ pT(qTr) v pT(rTq) v pTq & r. From B2 by B1 and Substitution.
T11. (pT(qTr)) → (pTr). Transitivity of »and then». From (1) by PL.
(1)  ~(tT~p) ↔ ~(pT~p) & ~(~pT~p). From B1 and PL.
(2)  ~(pT~p) & ~(~pT~p) → (pTp) v (~pTp). From T2 and PL.
(3)  (pTp) v (~pTp) ↔ (tTp). From B1.
T12. ~(tT~p) → (tTp). From (1) – (3) by PL.

    Of the above theorems all but T11 are valid for »and next» too. But the following difference between the two connectives should be noted. The four disjuncts in T1 and T2 are exhaustive of »logical space» both for »T» = »and next» and for »T» = »and then». But only for »T» = »and next» are the four disjuncts also mutually exclusive. For this reason it is not possible in the calculus of »and then» to replace a negated atomic T-expression by a disjunction of unnegated ones.⁴ And this again is the (formal) reason, why the important notion of a history has no counterpart in the logic of the connective »and then».
   4. The connective »and then» may be said to contain, in a concealed form, a temporal quantifier. »p and then q» , we said (above p. 3), means »p and at some later time q».
   It is, in fact, possible to define within our calculus the notions of always (»now and at all later times»), sometime(s) (»now or at some later time»), and never (»not now nor at any later time»).
   The expression p & ~(tT~p), where t is an arbitrary tautology of PL, says that it is (now) the case that p and not the case that at some later time it is the case that ~p. Hence the expression says that it is and always will be the case that p. We shall for this introduce the shorthand expression ∧p.
The expression ~(p & ~(tT~p)) is the denial of the above expression. It thus says that it either is (now) the case that ~p or is at some later time the case that ~p. It is equivalent to the expression ~p v (tT~p). We shall introduce for it the shorthand ∨~p. We thus have ~∧p ↔ ∨~p. Substituting ~p for p we obtain the equival­ence ~∧~ p ↔ ∨p . ∨p thus says that it is sometimes, either now or later, the case that p.
   ∧~p, finally, says that it is never, neither now nor later, the case that p.
   It is important to note that none of the temporal quantifiers is a primi­tive of our calculus. They are all defined in terms of the primitive »and then» (and truth-functional notions).
   We list a number of theorems for the temporal quantifiers:
T13.  ∧t. t is an arbitrary tautology of PL.
T14.  ∧p → p.
T15.  ∧p → ∨p.
T16.  ∧(p & q) ↔ ∧p & ∧q.
T17.  ∧(p → q) → (∧p → ∧q).
T18.  ∧p → ∧∧p.
T19.  ∨∧p → ∧∨p.
T20.  ∧(∧p → ∧q) v ∧(∧q → ∧p).

    The proofs use the »auxiliary» theorems which we proved in the pre­vious section, and no others.
    ∧t is an abbreviation for t & ~(tT~t). This is, by PL, equivalent with ~(tT~t) alone which, by virtue of B4 and Extensionality, is a theorem.
   p & ~(tT ~p) → p is true in PL. Hence ∧p → p is a theorem.
    Similarly, p & ~(tT~p) → pv (tTp) is true in PL. Hence ∧p → ∨p is a theorem.
   T16 with »∧» is an abbreviated form of p & q & ~(tT~(p & q)) ↔ p & ~(tT~p) & q & ~(tT~q). By virtue of B1 and PL the left membrum is equivalent with p & q & ~(tT~p) & ~(tT~q) which is equivalent with the right membrum.
    T17 can also be written ∧(p → q) & ∧p → ∧i. This, by virtue of T15 and Extensionality, is equivalent with ∧(p & q) → ∧q which imme­diately follows from T16.
   T18 with »∧» is an abbreviation for p & ~(tT~p) → p & ~(tT~p) & ~(tT~(p & ~(tT~p))). By virtue of B1 (and PL), ~(tT~(p & ~(tT~p))) is equivalent with     ~(tT~p) & ~(tT(tT~p)). The consequent, therefore, can be simplified to p & ~(tT~p) & ~(tT(tT~p)). But, by virtue of T11, tT(tT~p) entails tT~p. Hence the consequent can be further simplified to p & ~(tT~p) which makes it identical with the antecedent. Herewith the theorem is proved.
   ∨∧p → ∧∨p is an abbreviation of (p & ~(tT~p)) v (tT (p & ~(tT ~p))) → (p & ~(tT(~p & ~(tTp)))) v (tTp) & ~(tT (~p & ~(tTp))). We prove this formula by showing that each one of the disjuncts in the antecedent is inconsistent with the negation of the consequent. We first show that (p & ~(tT~p)) & (~pv (tT(~p & ~(tTp)))) & (~(tTp) v (tT(~p & ~(tTp)))) is a contradiction. This we do by showing that p & ~(tT~p) & ~p & ~(tTp) and p & ~(tT~p) & ~p & (tT(~p & ~(tTp))) and p & ~(tT~p) & (tT(~p & ~(tTp))) & ~(tTp) and p & ~(tT~p) & (tT(~p & ~(tTp))) & (tT(~p & ~(tTp))) are contradictions. The first is a contradiction, because p & ~p is a contradiction. The second is a contradiction for the same reason. The third contains as a conjunct ~(tT~p) and entails, by virtue of T8, tT~p. It therefore is a contradiction, since ~(tT~p) & (tT~p) is a contradiction. The fourth is a contradiction for the same reason. We next show that (tT(p & ~(tT~p))) & (~pv (tT(~p & ~(tTp)))) & (~(tTp) v (tT(~p & ~(tTp)))) is a contradiction. This we do by showing that (tT(p & ~(tT~p))) & ~p &  ~(tTp) and (tT(p & ~(tT~p))) & ~p & (tT(~p & ~(tTp))) and (tT(p & ~(tT~p))) & (tT(~p & ~(tTp))) & ~(tTp) and (tT (p & ~(tT~p))) & (tT(~p & ~(tTp)))

are contradictions. The first is a contradiction because it contains ~(tTp) and entails tTp. The second entails (tT~(tTp)) & (tT~(tT~p)). This, by virtue of B2, is equivalent with tT~(tTp) & ~(tT~p) v ~(tTp)T~(tT~p) v ~(tT~p)T~(tTp). But ~(tTp) & ~(tT~p) is a contradiction, since ~(tT~p), by virtue of T12, entails tTp which contradicts ~(tTp). ~(tTp)T~(tT~i) is a contradiction, since, by virtue of T3, it entails ~(tTp) and, by T8 and T12, tT(tTp) which, by T11, entails tTp. For the same reason, ~(tT~p)T~(tTp) is a contradiction. Hence, by B4, tT~(tTp) & ~(tT~p) v ~(tTp)T~(tT~p) v ~(tT~p)T~(tTp) is a contradiction. The third and the fourth conjunctions too entail (tT~(tTp)) & (tT~(tT~p)). Thus they too are contradictions. – Herewith T19 has been proved.
    T20 or ∧(∧p → ∧q) v ∧(∧q → ∧p) we prove by showing that its negation, ~∧(∧p → ∧q) & ~∧(∧q → ∧p) is a contradiction.
    The last formula is short for [p & ~(tT~p) & ~(q & ~(tT~q)) v (tTp & ~(tT~p) & (~qv (tT~q)))] & [q & ~(tT~q) & ~(p & ~(tT~p)) v (tTq & ~(tT~q) & (~pv (tT~p)))].
   After distribution this becomes a 4-termed disjunction of conjunctions [p & ~(tT~p) & ~(q & ~(tT~q)) & q & ~(tT~q) & ~(p & ~(tT~p))] v [(tTp & ~(tT~p) & (~qv (tT~q))) & q & ~(tT~q) & ~(p & ~(tT~p))] v [p & ~(tT~p) & ~(q & ~(tT~q)) & (tTq & ~(tT~q) & (~pv (tT~p)))] v [(tTp & ~(tT~p) & (~qv (tT~q))) & (tTq & ~(tT~q) & (~pv (tT~p)))]. We show that all four disjuncts are self-contradictory.
    a. After further distribution, the first of the four disjuncts becomes [p & ~(tT~p) & ~q v p & ~(tT~p) & (tT~q)] & [q & ~(tT~q) & ~p v q &  ~(tT~q) & (tT~p)]. The first disjunct in the left-hand conjunct contains ~q and hence it contradicts both disjuncts in the right-hand conjunct which contain q. The second disjunct to the left contains tT~q and hence it contradicts both disjuncts to the right which contain ~(tT~q).
    b. The second of the four disjuncts becomes after distribution, [(tTp & ~(tT~p) & ~q) v tTp & ~(tT~p) & (tT~q)] & [q & ~(tT~q) & ~p v q & ~(tT~q) & (tT~p)]. The first disjunct to the left entails, by virtue of T8, tT~q and hence it contradicts both disjuncts to the right which contain ~(tT~q). The second disjunct to the left entails, by virtue of T8, tT(tT~q) which, by virtue of T11, entails tT~q. Hence it too contradicts both disjuncts to the right.
    c. The third of the four disjuncts is self-contradictory for exactly the same reasons as the second. (We only have to interchange »p» and »q».)

    d. The fourth of the four disjuncts becomes, after distribution, [(tTp &     ~(tT~p) & ~q) v (tTp & ~(tT~p) & (tT~q))] & [(tTq & ~(tT~q) & ~p) v (tTq & ~(tT~q) & (tT~p))]. The conjunction of the first disjunct to the left and the first disjunct to the right entails, by virtue of B2, tTp & ~(tT~p) &  ~q & q & ~(tT~q) & ~p v (p & ~(tT~p) & ~qTq & ~(tT ~q) & ~p) v (q & ~(tT~q) & ~pTp & ~(tT~p) & ~q). But p & ~(tT~p) & ~q & q & ~(tT~q) & ~p is a contradiction, since it contains p & ~p (and also q & ~q). p & ~(tT~p) &   ~qTq & ~(tT~q) & ~p again is a contradiction, since, by virtue of T3 and T7, it entails ~(tT~p) but also entails, by virtue of T6 and T8, tT~ p. For the same reason (exchanging »p» for »q») q & ~(tT~q) & ~pTp & ~(tT~p) & ~q is a contradiction. Since all three disjuncts to the right of the first »T» in the above longer expression are contradictions, it is itself a contradiction (by virtue of B4). By similar argument it is shown that the conjunction of the second disjunct to the left and the first disjunct to the right yields a contradiction. ― Now consider the conjunction of the first disjunct to the left and the second to the right. It entails, by virtue of B2, tT(p & ~(tT~p) & ~q & q & ~(tT~q) & (tT~p) v (p & ~(tT~p) & ~qTq & ~(tT~q) & (tT~p)) v (q & ~(tT~q) & (tT~p) Tp & ~(tT~p) & ~q). The three disjuncts to the right of the first »T» in this expression are all of them contradictions: the first because it contains q & ~ q; the second because it entails ~(tT~p) but also tT(tT~p) which entails tT~p; and the third because it entails ~(tT~q) and also entails tT~q. Hence the longer expression too is a contradiction, by virtue of B4. ― Finally, consider the conjunction of the second disjunct to the left and the second to the right. By virtue of B2, it entails tTp & ~(tT~p) & (tT~q) & q & ~(tT~q) & (tT~p) v (p & ~(tT~p) & (tT~q) Tq & ~(tT~q) & (tT~p)) v (q & ~(tT~q) & (tT~p) Tp & ~(tT~p) & (tT~q)). The three disjuncts to the right of the first »T» are all of them contradictions: the first because it contains ~(tT~p) and tT~p (and tT~q and ~(tT~ q)); the second because it entails both ~(tT~p) and tT~p; and the third because it entails both ~(tT~q) and tT~q. Hence the longer expression too is a contradiction, by virtue of B4. ― Herewith T20 has been proved.
    5. In addition to the usual inference rules of substitution and detach­ment, our calculus embodies the Rule of Extensionality to the effect that provably equivalent expressions are interchangeable salva veritate.
   In the standard systems of modal logic extensionality can be proved with the aid of the Rule of Necessitation which says that a provable for­mula may become »necessitated».
    In quantification theory (the predicate calculus) again extensionality

is proved from the Rule of Generalization (for the introduction of quanti­fiers into a formula).
    The analogue of the Rule of Necessitation in our calculus would be a principle to the effect that, if f is a theorem, then ∧f is a theorem too. (»What is provably true is always true».)
   It is easy to prove that this principle holds true for our calculus. Assume that f were a theorem. Since ∧t is a theorem (T13), f ↔ ∧t would then also be a theorem. (All theorems are provably equivalent.) Hence, by the Rule of Extensionality, ∧f would be a theorem.
   6. From our calculus we pick out the following ingredients:
   B0, T14, T17, T18, T20, the inference rules of substitution and detach­ment, and the principle which says that, if f is a theorem, then ∧f is a theorem, too.
The sub-calculus constituted by these ingredients is structurally identical with the system of modal logic known as S4.3.
   If in the sub-calculus we could derive as theorems B1–B4, we should have shown that the calculus of the connective »and then» is structurally identical with the modal system S4.3. This derivation, however, is not possible.
   Consider a modal system with the following axiomatic basis:
C0.  A set of axioms of PL.
C1.  Nt.
C2.  ~N~t.
C3.  Np & Nq ↔ N (p & q).
C4.  Np v Nq ↔ N (pvq) & N (pvNq) & N (qvNp).
     The rules of inference are: substitution, detachment, and extensionality. ― »N» is read »it is necessary that». »M» is read »it is possible that». By definition »M» = »~N~». »t» is an arbitrary tautology of PL.
    If we adopt the following principle of translation: »Np» = »~(tT~p)», we can prove that the modal system C is structurally identical with the calculus of »and then».
   If we replace C3 by the principle N (p → q) → (Np → Nq) and the Rule of Extensionality by the Rule of Necessitation, and omit C1, we get an alternative axiomatization of this modal logic.
   7. Consider the expression p → (tTp). It says that, if it is the case that p, then, at some later time too, it is the case that p. If this were always so, then, if it were the case that p, it would again and again be the case that p — an infinite number of times. For this reason I shall say that the conjunction p & ∧(p → (tTp)) expresses the idea of an infinite recurrence (or return) of the presently occurring state of affairs that p. If

(a) ∧(p → (tTp))

were an axiom or theorem of our calculus, which it is not, then it would express the idea that whatever occurs, at any time, will infinitely recur, i.e. return infinitely many times after that.
    What is here called infinite recurrence must be distinguished from what I shall call perpetual recurrence (or return). A state of affairs will be said to recur perpetually, if and only if, should it occur at some time, it will always thereafter recur. The symbolic expression for this idea is

(b) ∨p → ∧(tTp).

Since (tTp) entails ∨p, (b) can also be written in the form ∨p → ∧((tTp) & ∨p). This, by virtue of T16, is equivalent with ∨p → ∧(tTp) & ∧∨p which, by virtue of PL, entails ∨p → ∧∨p. This last is struc­turally identical with the characteristic axiom of the modal system S5. If, in other words, we added (b) as an axiom to our calculus of the con­nective »and then», this would contain a structural equivalent of S5.
   Since p entails ∨p and ∧(tTp) entails tTp, it follows that (b) entails p → (tTp). Thus if (B) were an axiom, p → (tTp) would be a theorem and, consequently, ∧(p → (tTp)) or (a) would be a theorem too. Perpetual recurrence entails infinite recurrence, but not vice versa. The reason, why the entailment does not hold both ways, has to do with the nature of the time-medium. If time is dense or continuous, then it may happen that some state of affairs occurs infinitely many times before a certain future time, but never after that time. If, however, time is discrete, then this contingency cannot arise. Then, if a state recurs infinitely many times, it will always recur.
    The idea that everything which occurs will perpetually recur is well known from the history of metaphysical speculation. It seems to have been entertained by some Greek and Hellenistic philosophers. Not very long ago it was given a notable revival by Nietzsche. The idea that (B) is a necessary truth could therefore also be called the Axiom of Nietzsche.
    8. The temporal connectives »and next» and »and then» could be called forward-looking connectives. They relate states of affairs, which obtain at some arbitrary time, to some future states.
   To the forward-looking connectives there correspond backward-looking ones.
    The backward-looking counterpart of »and next» is the connective »next after». »pTq» is now to be read »p next after q». Another verbal expression for it is »and immediately before». »pTq» is then read »p and immediately before q». This last must not be confused with the meaning of »p before q».
   The nearest equivalent in ordinary language to the backward-looking counterpart of »and then» is the phrase »and before». The thought that

the state of affairs that p is there now and that the state that q was there earlier can be expressed in the words »p and before q».
   It is obvious that the axiom-system A0–A4 is valid equally for »and next» and for its backward-looking counterpart, and that B0–B4 is valid equally for »and then» and for its backward-looking counterpart.
    We could distinguish between the forward- and the backward-looking connectives by means of two symbols T→ and ←T [Filosofia.fi transcription changes for T→ and ←T: in the original, the arrows are above the symbol T]. We would then have 4 calculi: the calculus A0–A4 for T→ and its »mirror-image» for ←T, and the calculus B0–B4 for ←T and its »mirror-image» for T→.
    One could then proceed to combining the calculi in various ways. The combination of A0–A4 for T→ with A0–A4 for ←T would require the introduction of two axioms to the effect that (pT→ (q←Tr)) ↔ (p & rT→q) and (p←T (qT→r)) ↔ (p & r←Tq). The combination of B0–B4 for T→ with B0–B4 for ←T again would require axioms to the effect that (pT→ (q←Tr)) ↔ ((p & rT→q) v (pT→ (rT→q)) v (p←Tr) & (pT→q)) and (p←T (qT→r)) ↔ ((p & r←Tq) v (p←T (r←Tq)) v (pT→r) & (p←Tq)). We shall not, however, in this paper study in detail the combined calculi.

1 »And Next». Acta Philosophica Fennica 18, pp. 293-304. Helsinki 1965.
2 A2 may become replaced by the simpler axiom (pTq ) & (pTr)→(pTq & r).
3 The new axiom (pTq) & (rTs) ↔ (p & rTq & s v (qTs) v (sTq)) may become simplified to (pTq) & (pTr) ↔ (pTq & r v (qTr) v (rTq)). If we weaken the equivalence to a one-way implication (pTq) & (pTr) → (pTq & r v (qTr) v (rTq)), we need an additional axiom in order to strengthen it into an equivalence. This additional axiom could be given in the form of a principle of transitivity pT (qTr) → (pTr).
4 »And Next», p. 296.

Communicated April 18, 1966 Printed June, 1966

Keskuskirjapaino — Centraltryckeriet
Helsinki — Helsingfors