Two (sound) axiom systems for linear temporal logic

(CW: mathematical logic.)

Current mood: looking up proof-theoretic treatments of linear temporal logic. (The LTL I encountered in university, primarily in concurrency-related courses, was approached model-theoretically and didn't describe how to prove program properties outside of brute force.)

Alas, it turns out that there are no finitistic (i.e. having decidable axioms) axiomatisations of LTL in general [Sz86]. (This should not be surprising, given that the model-theoretic definition of LTL relies upon the structure of the natural numbers, and hence that we encroach upon Gödelian territory.) It's unclear from my initial research whether this incompleteness result extends to the more restricted case of Boolean/propositional LTL with finite state.

In this post I consider two attempts to axiomatise the most important properties of LTL in a way conducive to proving simple program properties, and show that despite their similar structure, one is a strict logical consequence of the other.

---

Consider the usual Boolean propositional logic augmented with two modal operators \(\Box\) (always / from now on) and \(\bigcirc\) (next / tomorrow), where \(\Box\) behaves like a reflexive normal modal logic, i.e.:

• Tautologies are \(\Box\) true: if \(\vDash P\) then \(\vDash \Box P\)
• \(\Box\) is distributive: \(\Box (P \rightarrow Q) \rightarrow (\Box P \rightarrow \Box Q)\)
• \(\Box\) is reflective: \(\Box P \rightarrow P\)

Additionally, assume the following axioms:

• \(\bigcirc\) distributes over \(\land, \lor, \lnot\): \(\bigcirc (P \land Q) \leftrightarrow \bigcirc P \land \bigcirc Q\), etc.
• \(\Box\) and \(\bigcirc\) commute: \(\Box \bigcirc P \leftrightarrow \bigcirc \Box P\).

  (This corresponds to the equivalence between From now on, the following day, \(P\) and From tomorrow on, \(P\).)

Now, consider the following pairs of axioms, both of which aim to capture the sequential intuition of LTL: \[\begin{align} \Box P & \rightarrow (P \land \Box \bigcirc P) \tag{X1} \\ (P \land \Box \bigcirc P) & \rightarrow \Box P \tag{X2} \\ \\ \Box P & \rightarrow \Box \bigcirc P \tag{Y1} \\ \Box (P \rightarrow \bigcirc P) & \rightarrow (P \rightarrow \Box P) \tag{Y2} \end{align}\]

\(X1\) and \(X2\) collectively state that from now on is equivalent to today and from tomorrow on.

\(Y1\) is a weakening axiom asserting that from now on implies from tomorrow on. \(Y2\) is what [Fi02] describes as the induction axiom for linear temporal logics: if it's true today and it never stops being true overnight, it's always true.

Claim: \(X1, X2\) is strictly weaker than \(Y1, Y2\).

Proof: \(X1\) and \(Y1\) are clearly equivalent (given reflectivity of \(\Box\)).

\(Y1, Y2 \vDash X2\): Assume \(P, \Box \bigcirc P\); then \(\Box (P \rightarrow \bigcirc P)\) by conditional introduction + distributivity of \(\Box\) over \(\land\). The result follows from \(Y2\).

strictly (sketch): Consider (degenerate) interpretations where \(\bigcirc\) is the identity modal operator. (I.e. \(\bigcirc P \leftrightarrow P\).) These satisfy \(X1, X2\) trivially. But \(Y2\), which is equivalent to \(P \rightarrow \Box P\), doesn't follow.

References:

[Fi02] Fisher, M. (2002). An Introduction to Practical Formal Methods using Temporal Logic. Retrieved from http://cgi.csc.liv.ac.uk/~michael/TLBook/tl4-4up.pdf 22/10/2014.
[Sz86] Szalas, A. (1986). Concerning the semantic consequence relation in first-order temporal logic. Theoretical Computer Science, 47, 329-334.