"Always"

”Always”

1. In previous papers I have studied the logic of two temporal binary connectives corresponding roughly to the phrases ”and next” and ”and then” in ordinary language.¹ Use of the first connective presupposes that time is a succession of discrete moments or stretches of time; use of the second is independent of this assumption of discreteness. There are many divisions of time into discrete ”bits”—for example, into years or days or seconds. Meaningful use of ”and next” in a context is relative to some such division of time, but it imposes no specific requirements on the absolute or relative length of the bits.
The calculus of ”and next” has the following vocabulary:
 

a. Variables p, q, r, … (an unlimited supply).
b. Truth-connectives ~, &, v, →, and ↔ for negation, conjunction, disjunction, (material) implication, and (material) equivalence respectively.
c. A binary connective T (”and next”).
d. Brackets.
e. An auxiliary constant t, representing an arbitrary tautology of propositional logic (PL).

The well-formed formulae (wffs) of the calculus are defined recursively as follows:

 

 

i. A variable is a formula.
ii. A wff in brackets preceded by ~ is a wff; two wffs
in brackets joined by &, v, →, ↔, or T form a wff.

 

 

For the sake of saving brackets we introduce the convention that the order of “binding force” of the connectives shall be: ~, &, v, →, ↔, T. ~ is the weakest and T the strongest connective.
  For the sake of convenience we shall use autonymously in the meta-language, not only the signs for constants (b-e), but also the signs for variables (a). Occasionally we shall use the meta-variables f, g and h to represent arbitrary formulae (wffs) of the calculus.
The axioms of the calculus are:

A0.    A set of axioms of PL.
A1.    (pvqTrvs)↔(pTr)v(pTs)v(qTr)v(qTs).
A2.    (pTq)&(pTr)→(pTq&r).
A3.    p↔(pTqv~q).
A4.    ~(pTq&~q).

The rules of inference, finally, are:

R1.    Substitution of wffs for variables.
R2.    Detachment (modus ponens).
R3.    Replacement of a wff by a provably (in the calculus) equivalent wff. (Rule of     Extensionality.)

By the universe of a given T-expression we understand the set of variables p, q, … which occur 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(...)))..., where each occurrence of ”-” represents an occurrence of a state-description in a given universe, the first sequence of dots 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 successive state-descriptions in it. The total number of possible histories of length m in a universe of width n is 2^{m n}.
   It may be shown that every T-expression is provably equivalent with a disjunction of histories (of equal length) in the universe of the expression. 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 disjunction 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^{m n} different ways (enumerating them all). What the expression says is then 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 can be shown that the calculus of the connective ”and next” is, in the sense defined, semantically complete.
   We list the following theorems which will be needed for the proofs, to be given later, of some theorems concerning the notion ”always”:

T1.    (p&qTr&s)↔(pTr)&(qTs).²
T2.    ((pTq)Tr)↔(pTq&r).
T3.    (pTq)↔(p&(tTq)).     (From this immediately follows (pTq)→p.)    
T4.    ~(pTq)↔(pT~q)v(~pTq)v(~pT~q).    

We shall also make use of the following meta-theorem in the proofs of theorems: 

 

M. If a formula of the form f →g is provable in the T-calculus, then (hTf)→(hTg) is also provable.

The truth of M follows immediately from R3 and the meta-theoretic equivalent of T1.

 

 

    2. For the sake of notational economy, let us use the same symbol ”T” for ”and then”, too. The vocabulary and formation rules of the calculus of ”and then” are then the same as those of the calculus of ”and next”. Of the above axioms (A0), A1, A3, and A4 obviously hold also for ”and then”. Equally obviously, A2 does not hold. If it is now the case that p and then, i.e. later, is the case that q and also then is the case that r, it does not follow that the conjunction of these later states must ever be true. They may, but need not, occur together. It is also possible that one of them occurs first and then the other. If this exhausts the possibilities, time is a linear order of moments or stretches. An axiom system of the connective ”and then” under the assumption of a linear time-order is the following:

B0.    = A0.
B1.    = A1.
B2.    (pTq)&(pTr)↔(pTq&rv(qTr)v(rTq)).
B3.    = A3.
B4.    = A4.

The rules of transformation are R1–R3.
The calculus of ”and then” does not require that time be a discrete medium. The order of moments in time can be discrete or dense (compact) or continuous.
We can replace B2, the Axiom of Linearity, by another, stronger or weaker, axiom. One interesting alternative to B2 would be an Axiom of Transitivity: (pT(qTr))→(pTr). An order of time which obeys the principle of transitivity, but not that of linearity, can be ”branching”. In this time two states which happen after a given one are not necessarily ”comparable” with regard to their mutual relation in time. Time in a relativistic universe has this structure. —Another alternative to B2 would be an Axiom of Circularity or of ”Perpetual Return”, pv(tTp)→~(tT~(tTp)). A time of this structure is so constituted that whatever occurs in it will always recur at some later moment.
   3. The calculus of ”and then” can be said to contain, in a concealed form, a temporal quantifier. The expression p&~(tT~p)

 

 

 

says that it is now the case that p and not at any later time the case that not-p. Thus it says that it is (now and) always (in the future) the case that p. We can introduce the abbreviation ∧p for p&~(tT~p). It is sometimes the case that p, if and only if, it is not always the case that not-p. ~(~p&~(tT~~p)), or ~∧~p, is equivalent with pv(tTp). As an abbreviation for this we shall    
also write ∨p.
   We can prove the following theorems for ”always”:

T5.    ∧(p&q)↔∧p&∧q.        
T6.    ∧p→∧∧p.
T7.    ∧(∧p→∧q)v∧(∧q→∧p).
T8.    ∧p→p.
T9.    ∧t.
    
The fragment of the calculus of ”and then”, which has as axioms B0, T5–T9, and as rules of inference R1–R3 is structurally isomorphic with the system of modal logic S4.3.
   We replace T8 (as axiom) by the weaker principle ~∧~t and  re-define ∧p as meaning ~(tT~p), i.e. as meaning that it is always in the future the case that p. The weakened form of (the tense-logical analogue of) S4.3 which we then get is structurally isomorphic with the calculus of ”and then”. In it we can define the  connective T by means of the temporal quantifier ∧, as follows: pTq=_df p&~∧~q.
    4. In the calculus of ”and next” we cannot define the notions of ”always” and ”sometimes”. If we want to introduce them into the calculus, we must introduce a new primitive. We shall take as primitive the notion of now and always in the future and use for it, as before, the symbol ∧. ∧p thus signifies a history of denumerably infinite length of a world which is and unchangingly remains in the state that p. The symbol ∨ we regard as an abbreviation for ~∧~ .∨ p, i.e. ~∧~p, means that either now or at some time in the future it is the case that p.
   For purposes of forming well-formed formulae ∧ functions exactly like the unitary connective ~. In order to save brackets we have the convention that, when ∧ is attached to a variable or   

 

 

 

to a formula of the form ~f, the variable and the formula need not be enclosed in brackets. We also have the convention that when ~ is attached to a formula of the form ∧f, the formula need not be enclosed in brackets.
    It is obvious that T5–T9 above hold true in the calculus of ”and next” embellished with a temporal quantifier. But since the temporal quantifier (∧) cannot be defined with the aid of the temporal connective (T), we cannot prove theorems about ”always” from the axioms about ”and next” alone. How shall we therefore incorporate T5–T9, and other logical truths about ”always”, into the axiomatized calculus?
   One possibility would be to add to the axioms A0–A4 special axioms for ”always”. One could, for example, take T5–T9 as additional axioms. A huge number of new theorems could then be proved. Could we prove all formulae which hold true for ”always” in the calculus of ”and next” thus enlarged?
    The answer is negative. A calculus with the axiomatic basis A0–A4 + T5–T9 + R1–R3 would be semantically incomplete with regard to a residue of logical truths, viz. those truths which are specific to discrete time. Examples of such truths are:

T10.    ∧p↔(pT∧p).
T11.    ∧(tTp)↔(tT∧p).
T12.    (pT∨~p)→∨(pT~p).

The first theorem says that it is from now on always the case that p, if and only if, it is now the case that p and from the next moment on is always the case that p. For T=”and then” the implication holds from left to right, but not from right to left.
   The second theorem says that it is now and always true that it is next the case that p, if and only if, it is from the next moment on always the case that p. For T=”and then” the implication holds neither way.
   The third theorem, finally, says that, if it is now the case that p but at some future moment this is no longer the case, then there is a pair of successive moments, in the first of which it is the case that p and in the second of which it is not the case that p. In

 

 

 

other words: if something ceases to exist in discrete time, then there is a last moment in which it exists (is) and a first moment in which it does not exist (is not).
   The question may be raised whether the addition of T10–T12 to the axioms for T would constitute a semantically complete axiomatics for the calculus of ”and next” and ”always”. I shall not discuss this question here. Instead I shall explore another method for proving theorems in the quantified logic of discrete time.
    5. First a number of auxiliary notions must be defined.    
    By the scope of a ∧ we understand the wff to which it is attached: f in -∧(f)-. (Read ”∧” as ”quantifier”.)
   A ∧ is of ∧-degree 1, if and only if, in the scope of this ∧ there is no other ∧.
   A ∧ is of ∧-degree n, if and only if, in the scope of this ∧ there is at least one ∧ of ∧-degree n – 1 and no ∧ of higher ∧-degree than n – 1.
   By the scope of a T, we understand the wff to its right: f in -T(f)-.
    A T is of degree 1, if and only if, it is not in the scope of any other T.
    A T is of degree n, if and only if, it is in the scope of some T of degree n – 1 but not in the scope of any T of higher degree than n – 1.
   The T-degree of a formula is the degree of the T of highest degree, which occurs in the formula, plus 1. The T-degree of a formula which does not contain any T at all is 1.
    For convenience, we shall call a formula of T-degree 1 a ”one day formula”, and a formula of T-degree n a ”n day formula”.
    A ∧ which does not occur within the scope of any T in a formula of T-degree n, is said to be itself of T-degree n.
    A ∧ which occurs within the scope of some T of degree m in a formula of T-degree n, but not within the scope of any T of higher degree than m, is of T-degree n – m.
    It follows that a ∧ which occurs within the scope of some T of degree n – 1 in a formula of T-degree n is a ∧ of T-degree 1.    
    In a formula of T-degree n, quantifiers of T-degree n can be

 

 

called ”first day quantifiers”, and quantifiers of T-degree 1 ”last day quantifiers”.
   Examples. The formula printed below is of T-degree 5. It is thus a five days formula. The ∧-degrees of the quantifiers are indicated by a numeral above each quantifier, and the T-degrees of the quantifiers by a numeral below each quantifier. The degrees of the T's, finally, are indicated by a numeral below each T.

     3        1            21                              1      1
    (∧(pT(∧q→(rT∧∧s))))→(pT(qT(~∧rT(∧sTu))))
           1              2                     1    2         3     4
     5        4            33                             3      2

The quantifier to the extreme left is a first day quantifier. The formula contains no last day quantifier.
    6. Let there be a formula of T-degree n. Consider k successive moments (”days”) in discrete time. (k>n.) We assume that the formula contains one or more occurrences of ∧.
    What the formula with quantifiers ”says” of the time-span of k successive moments can also be expressed by a formula without quantifiers. We shall call the second formula the k-reduced counterpart or k-model of the first formula. If k equals the T-degree n of the unreduced formula, the k-model will also be called the minimal model of the unreduced formula.
    The reduction of a given formula of T-degree n to a k-model is performed according to the following rule:
   Replace every part of the form ∧(f) by k – n + m – g + 1 successive occurrences fT(fT(...))... of the formula f in the scope of the quantifier. Here m is the T-degree of the quantifier and g the T-degree of the formula f in its scope.
If ∧ is a first day quantifier, then m = n. If the scope of ∧ does not contain the symbol T, i.e. if the scope is a formula of PL simply, then g = 1. A first day ∧ the scope of which is a formula of PL we thus eliminate by simply replacing it and the formula in its scope by k successive occurrences of the scope.
When a quantifier occurs in the scope of another quantifier, the elimination of quantifiers has to take place in successive steps.

 

 

 

But it is immaterial whether we first eliminate a quantifier of higher ∧-degree and then one of a lower ∧-degree, or vice versa. We shall illustrate this by means of an example:
   Let the formula be ∧∧p and the task to construct a 3-model for it. In the formula, as given, the left-most ∧ is of degree 2 and of T-degree 1. The second ∧ is of ∧-degree 1 and of T-degree 1. The T-degree of the formula itself is 1 and the T-degree of the scopes of the two quantifiers is, of course, also 1. If we first eliminate the higher degree ∧, we have to replace the whole formula by 3 (= 3 – 1 + 1 – 1 + 1) successive occurrences of the formula in the scope of that ∧. This gives us the formula ∧pT(∧pT∧p). In this formula, which is of T degree 3, all three quantifiers are of ∧-degree 1. The first (left-most) is of T-degree 3, the next of T-degree 2, and the last of T-degree 1. The scopes of each ∧ is of T-degree 1. The first ∧ ought therefore to be replaced by 3 successive occurrences of its scope. (3 = 3 – 3 + 3 – 1 + 1.) The second is replaced by 2 occurrences of its scope. (2 = 3 – 3 + 2 – 1 + 1.) And the third is replaced by 1 occurrence of its scope, i.e. by the scope itself. (1 = 3 – 3 + 1 – 1 + 1.) These replacements yield the formula pT(pTp)T((pTp)Tp). After repeated applications of T2 (and R3) to this formula, it is simplified to pT(pTp).
    We could also first have eliminated the ∧ of lower ∧-degree in ∧∧p. This would have been a quicker way to the end, the 3-model. We then replace the ∧ to the right in ∧∧p by 3 occurrences of the formula in its scope. This gives us the formula ∧(pT(pTp)). In it the remaining ∧ is of ∧-degree 1 and of T-degree 3. The elimination takes place by simply dropping the quantifier, leaving one occurrence of the formula in its scope. (1 = 3 – 3 + 3 – 3 + 1). This gives us the formula pT(pTp).
   We can test and decide whether or not the k-model of a given formula is a T-tautology. We adopt the following definition of logical truth for a formula containing temporal quantifiers: A formula is logically true, if and only if, for all values of k(≥ the T-degree n of the formula), the k-model of the formula is a T-tautology.
    7. Given a formula of T-degree n. Assume that it can be proved that

 

 

a) the minimal model of the formula is a T-tautology, and
b) if the k-model of the formula is a T-tautology, then the k + 1-model is a T-tautology, too.

From these premisses we conclude that the formula is logically true, i.e. that every k-model of it is a T-tautology.
   Consider two formulae, one of the form ∧(f) and one of the form fT∧(f), where the meta-variable f in both formulae represents the same wff of our calculus. Now replace the occurrence of ∧(f) in the second formula by the k-model of ∧(f). Clearly, the formula obtained after the replacement is the k + 1-model of the formula ∧(f).
   As we know, the k-model of a formula is obtained by replacing every part of the form ∧(f) which occurs in it by its k – n + m – g + 1-model. (The values of m and g may be different for different parts of this form.) Thanks to the above observation on the relation between formulae of the forms ∧(f) and fT∧(f), we can for any given formula construct another formula such that the k + 1-model of the first is obtained by substituting in the second for its quantified parts the appropriate counterparts from the k-model of the first formula. This fact is of crucial importance to the proof of theorems by induction.
    We prove a few sample theorems. The first is T5 ∧(p&q)↔∧p&∧q.
   The minimal model of the formula T5 is p&q↔p&q. This is a PL-tautology and hence also a T-tautology.
    All three quantifiers in the formula are of the same ∧-degree and of the same T-degree. Hence the k-model of the formula is obtained by replacing the three parts of the form ∧(f) by their k-models, i.e. by k successive repetitions of the formulae in the scopes of the quantifiers.
    Now consider the formula (p&qT∧(p&q))↔(pT∧p)&(qT∧q). If for its three components of the form ∧(f) we substitute their k-models, we obtain the k + 1-model of T5.
   The formula (p&qT(∧(p&q))↔(pT∧p)&(qT∧q) can also be written in the equivalent form (p&qT∧(p&q))↔(p&qT∧p&∧q).

 

 

If for its three quantified components we substitute their k-models, we again get the k + 1-model of T5. But if the k-model of T5 is a T-tautology, then the k-model of ∧(p&q) is provably equivalent, and hence by virtue of R3 interchangeable, with the conjunction of the k-model of ∧p and the k-model of ∧q. The k + 1-model obtained through substitution will therefore be a T-tautology, too. (Since it will be of the form (hTf)↔(hTf), where h represents p&q and f the k-model of ∧(p&q).)
    We next prove T6 ∧p→∧∧p.
    The minimal model of the formula is p→p which is a tautology.
Consider the formula (pT∧p)→((pT∧p)T∧∧p). If for the first two occurrences in it of ∧p we substitute the k-model of ∧p and for the component ∧∧p we substitute the k-model of ∧∧p, the formula which results from these substitutions is the k + 1-model of T6.
   By virtue of T2, (pT∧p)→((pT∧p)T∧∧p) may be transformed into (pT∧p)→(pT∧p&∧∧p). If the k-model of T6 is a T-tautology, the k-model of ∧p is equivalent with the conjunction of the k-model of ∧p and the k-model of ∧∧p. By virtue of R3, therefore, the formula which after substitution results in the k + 1-model of T6, will be a T-tautology, too. This completes the inductive proof of the theorem.
    We shall not burden the exposition here with proofs of T7, T8, or T9. But we shall prove the theorems T10, T11, and T12 which are peculiar to discrete time.
   The minimal model of T10 ∧p↔(pT∧p) is (pTp)↔(pTp) which is a tautology.
    Consider the formula (pT∧p)↔(pT(pT∧p)). If we replace ∧p in the left member of the equivalence by its k-model and ∧p in the right member by its k – 1-model, we obtain the k + 1-model of T10. (It should be noted that both quantifiers in T10 are of ∧-degree 1, but that the first is of T-degree 2 and the second of T-degree 1.) Instead of saying that we replace ∧p in the right member by its k – 1-model, we can also say that we replace the component pT∧p (in this right member) by its k-model.
   Assume that the k-model of T10 is a T-tautology. Then the

 

 

k-model of ∧p and the k-model of pT∧p are provably equivalent and, by virtue of R3, interchangeable. The formula which, after the above replacements in (pT∧p)↔(pT(pT∧p)), is the k + 1-model of T10 will therefore be a T-tautology, too.
  Finally, we prove T12 or the formula (pT∨~p)→∨(pT~p).
   We replace the symbol ∨ for ”sometimes” by the symbol ∧ for ”always” according to their definitions. We get the new formula (pT~∧p)→~∧~(pT~p). Its minimal model is (pT~p)→→~~(pT~p). This is a tautology.
    Consider the formula (pT~(pT∧p))→~(~(pT~p)T∧~(pT~p)). If in it we substitute for ∧p the k – 1-model of ∧p, and for ∧~(pT~p) the k-model of ∧~(pT~p), we obtain the k + 1-model of the formula T12.
    Now assume that the k-model of T12 is a T-tautology. This is equivalent to assuming that the k-model of pT~∧p tautologically entails the k-model of ~∧~(pT~p).
   By virtue of T4, negation-signs in front of T-expressions can be eliminated. When we apply this theorem to pT~(pT∧p) we get pT((pT~∧p)v(~pT∧p)v(~pT~∧p)). But by virtue of A3 (and A1 and R3), (~pT∧p)v(~pT~∧p) is equivalent with ~p alone. Thus the longer expression can be simplified to pT((pT~∧p)v~p) which, by virtue of A1, can also be written (pT(pT~∧p))v(pT~p).
   When we apply T4 to the outermost negation-sign in ~(~(pT~p)T∧~(pT~p)), we get (~(pT~p)T~∧~(pT~p))v((pT~p)T∧~(pT~p))v((pT~p)T(~∧~(pT~p)). By virtue of A3 (and A1), the disjunction of the second and third disjunct is equivalent with pT~p alone. The longer expression can thus be simplified to (~(pT~p)T~∧~(pT~p))v(pT~p).
   The formula of which we have to prove that it is a T-tautology, if the k-model of T12 is a T-tautology, is the k + 1-model of (pT(pT~∧p))v(pT~p)→(~(pT~p)T~∧~(pT~p))v(pT~p). But, since pT~p occurs in both the antecedent and the consequent, the task can be reduced to proving that the k + 1-model of (pT(pT~∧p))→(~(pT~p)T~∧~(pT~p)) is a T-tautology, if the k-model of T12 is one.
   By virtue of T4 (and A1 and A3), ~(pT~p) is equivalent with

 

 

(pTp)v~p. The consequent of the last implication-formula can thus also be written ((pTp)v~p)T~∧~(pT~p). By virtue of A1, this is equivalent with ((pTp)T~∧~(pT~p))v(~pT~∧~(pT~p)). The first disjunct is, by virtue of T1, equivalent with pT(p&~∧~(pT~p)) which, by virtue of T2, is equivalent with (pTp)&(pT~∧~(pT~p)). Thus the formula, the k + 1-model of which we have to prove to be a T-tautology, if the k-model of T12 is one, can also be written (pT(pT~∧p))→((pTp)&(pT~∧~(pT~p))v(~pT~∧~(pT~p)). But since the antecedent and the second disjunct in the consequent are incompatible with one another (the one entails p and the other ~p), our task can now become further simplified to that of proving that the k + 1-model of (pT(pT~∧p))→(pTp)&(pT~∧~(pT~p)) is a T-tautology, if the k-model of T12 is a T-tautology.
    By virtue of T3, pT~∧p entails p and by virtue of this fact and the meta-theorem M (p. 210) pT(pT~∧p) entails pTp. Now our task is reduced to that of showing that the k + 1-model of (pT(pT~∧p))→(pT~∧~(pT~p)) is a T-tautology, if the k-model of T12 is one. And this, by virtue of meta-theorem M, is reducible to the task of showing that the k-model of pT~∧p entails the k-model of ~∧~(pT~p), if the k-model of T12 is a T-tautology. But this as was noted above, is exactly what the assumption that the k-model of T12 is a T-tautology amounts to. Q.E.D.
   8. Is there a procedure by means of which it can be decided whether, on the assumption that the k-model of a given formula is a T-tautology, its k + 1-model is a T-tautology too? Can every formula which is such that all its k-models are T-tautologies be proved by the inductive method which we used in the preceding section?
   My conjecture is that the answer to both questions is affirmative, i.e. that the calculus of ”always” in discrete time is decidable and semantically complete with regard to its set criterion of logical truth.
    If we interpret ∧ as meaning necessity, we can extract from our calculus a modal logic which is stronger than S4.3 but weaker than S5. The question may be raised whether one can give to the

 

 

binary connective T a modal interpretation too, i.e. whether the entire calculus of ”always” can be interpreted as some (unorthodox) kind of modal logic. This is another question which I shall not discuss here.³

1 ”And Next”. Acta Philosophica Fennica 18, 1965. pp. 293—304.—”And Then”. Comm. phys.-math., Soc. Sci. Fenn. XXXII: 7, 1966.
2 In the original version of the calculus of ”and next” T1 figured as an axiom. It is easily shown, however, that it may be replaced by the weaker axiom A2 above.    
3 One can interpret the calculus of ”and next” as an ”unorthodox” modal logic. This can be done in several ways, moreover. One can, for example, interpret it as a modal logic of propositions which are, all of them, either necessary or impossible and never contingent. (Cf. my paper ”Quelques remarques sur la logique du temps et les systèmes modales”, Scientia 102, 1967.) The new problem is, whether both T and ∧ can be interpreted modally. This would require a modal calculus with two modal primitives in it.

 
Received on Jan. 19, 1968.