A temporal logic prover from Volpe’s work

The formulas are built from atoms, \(\bot\), \(\land\), \(\to\) and the four tense operators; \(\neg A\) is \(A \to \bot\). A frame is a set \(W\) of instants with a relation \(\prec\) (“earlier than”); a model adds a valuation of the atoms. At an instant \(w\):

• \(\mathbf{F}A\) is true iff \(A\) is true at some \(v\) with \(w \prec v\);
• \(\mathbf{P}A\) is true iff \(A\) is true at some \(v\) with \(v \prec w\);
• \(\mathbf{G}A\) is true iff \(A\) is true at every \(v\) with \(w \prec v\);
• \(\mathbf{H}A\) is true iff \(A\) is true at every \(v\) with \(v \prec w\).

The minimal tense logic \(K_t\) (Lemmon) is the set of formulas valid in every frame: it puts no condition on \(\prec\). Stronger logics are obtained by restricting the class of frames, or equivalently by adding axioms. Volpe’s table 2.4 lists the usual ones; those implemented in the prover are:

Each condition has a mirror image for the past (\(\mathbf{H}A \to \mathbf{HH}A\), \(\mathbf{P}A \to \mathbf{PP}A\) …). The prover knows four systems by name:

The conditions ser_r, ser_l, ser (both) and dens can be added to any system. They are independent of each other and compatible: the rationals satisfy all of them, and each combination has a model of its own (the integers are linear and unbounded but not dense, an interval of the rationals is dense but bounded, and so on). A word of warning on names: in Venema’s chapter [6], \(K_t\) already includes transitivity; here, as in Lemmon, Copeland and Volpe, it does not.

Volpe’s systems derive two kinds of formulas: labeled formulas \(b : A\) (“\(A\) is true at the instant \(b\)”) and relational formulas \(b < c\) (“\(b\) is earlier than \(c\)”). Premisses may be of both kinds; the conclusion is a labeled formula. An interpretation maps labels to instants, and \(\Gamma \models b : A\) means that every interpretation making \(\Gamma\) true makes \(b : A\) true.

The system \(N(K_t)\) (Volpe’s fig. 4.1) has the rules for \(\to\) and classical \(\bot\), and introduction and elimination rules for \(\mathbf{G}\) and \(\mathbf{H}\). The rules for \(\mathbf{F}\), \(\mathbf{P}\) and \(\land\) are derived (fig. 4.2); the prover uses them as primitive rules.

The label may change in \(\bot\)E: a contradiction at any instant yields anything at any instant. “Fresh” means that the label does not occur in the conclusion nor in any open assumption other than the discharged ones; \(\mathbf{G}\)I and \(\mathbf{F}\)E are the exact counterparts of \(\forall\)I and \(\exists\)E. Volpe proves \(N(K_t)\) sound and complete for \(K_t\) (theorems 4.4 and 4.5).

The properties of \(\prec\) are captured by rules that discharge relational assumptions (fig. 4.3 and section 4.2.3). Each has the form: from some relational premisses, and from a derivation of a labeled formula \(d : B\) in each branch under some relational assumptions, infer \(d : B\).

\(N(K_l) = N(K_t) + \) trans< \(+\) conn< is sound and complete for linear time; the extensions with ser and dens are sound and complete for the corresponding logics (theorem 4.8). Irreflexivity has no rule: it does not change the set of valid formulas (section 4.2.2). Completeness is stated for labeled premisses: from relational premisses alone no contradiction can be derived (from \(b < c\) and \(c < b\), for instance, \(N(K_l)\) does not derive \(b : \bot\)); Volpe’s systems \(N'(K_l)\) with an explicit relational theory (section 4.3) remove this limit.

Here is Volpe’s derivation of the density axiom, as the prover finds it (the eigenlabels of \(\mathbf{F}\)E and dens< are flagged [s], [t]):

 1  │ │ b : FQ                              AS
    │ ├────────
 2  │ │ │ [s] s : Q                         AS
 3  │ │ │ b < s                             AS
    │ │ ├────────
 4  │ │ │ │ [t] b < t                       AS
 5  │ │ │ │ t < s                           AS
    │ │ │ ├────────
 6  │ │ │ │ t : FQ                          FI 2,5
 7  │ │ │ │ b : FFQ                         FI 6,4
 8  │ │ │ b : FFQ                           dens< 3,4-7
 9  │ │ b : FFQ                             FE 1,2-8
10  │ b : FQ → FFQ                          →I 1-9

Run it in SWI-Tinker

The thesis goes much further: discrete time (an immediate-successor relation \(\lhd\), section 4.2.3), until-free LTL (4.2.4), the systems \(N'(K_l)\) with an explicit relational theory and their normalization (4.3), a treatment of until (4.4), branching time (bundled Ockhamist logics and BCTL*, chapter 5) and the mosaic method (chapter 6). Discrete time is the next candidate, because it matters for Diodorean modality: \(\Box A := A \land \mathbf{G}A\) gives S4.3 on dense time and S4.3.1 on discrete time.

For a sequent the prover first looks for a countermodel. It builds a labeled tree in the style of Jeffrey [7] and Copeland [8]: unsigned, with formulas and their negations at labelled instants, and the relations between instants written as lines of their own. Copeland’s tree system for \(K_t\) is extended with the rules for \(\land\), \(\mathbf{G}\) and \(\mathbf{H}\), with the rules of the chosen conditions on \(\prec\), and with Volpe’s labels. Here is the tree of a sequent that is not valid in linear time: from “\(Q\) will be the case” and “\(R\) will be the case” it does not follow that \(Q\) and \(R\) will be the case together. In \(K_l\) any two instants are comparable, hence the three branches of the rule conn (\(s < t\), \(t < s\), \(t = s\)):

1   b : FQ                                    premiss
2   b : FR                                    premiss
3   b : ¬F(Q ∧ R)                             denied conclusion
4   b < s                                     F 1 (new point s)
5   s : Q                                     F 1, 4
6   s : ¬(Q ∧ R)                              ¬F 3, 4
├─ 7   s : ¬Q                                 ¬∧ 6
│  ×  closed: 5, 7
└─ 8   s : ¬R                                 ¬∧ 6
   9   b < t                                  F 2 (new point t)
   10  t : R                                  F 2, 9
   11  t : ¬(Q ∧ R)                           ¬F 3, 9
   ├─ 12  s < t                               conn
   │  ├─ 13  t : ¬Q                           ¬∧ 11
   │  │  ○  open branch: countermodel
   │  └─ 14  t : ¬R                           ¬∧ 11
   │     ×  closed: 10, 14
   ├─ 15  t < s                               conn
   │  ├─ 16  t : ¬Q                           ¬∧ 11
   │  │  ○  open branch: countermodel
   │  └─ 17  t : ¬R                           ¬∧ 11
   │     ×  closed: 10, 17
   └─ 18  t = s                               conn
      ×  closed: 10, 8

Run it in SWI-Tinker

An open branch gives a countermodel: here \(b < s < t\), with \(Q\) true at \(s\) only and \(R\) at \(t\) only. Every countermodel is checked by a model checker, which evaluates the premisses and the conclusion and verifies the conditions of the frame. A countermodel shows, by soundness, that no derivation exists.

The tree rules mirror the rules of natural deduction: (\(\mathbf{F}\)) and (\(\mathbf{P}\)) introduce a new instant, as \(\mathbf{F}\)E and \(\mathbf{P}\)E introduce an eigenlabel; (\(\neg\mathbf{F}\)) and (\(\neg\mathbf{P}\)) run along an existing relation, as \(\mathbf{G}\)E and \(\mathbf{H}\)E; the denied conclusion, \(b : \neg A\) for a conclusion \(b : A\), is the assumption of classical \(\bot\)E; a closed branch is an application of \(\to\)E yielding \(\bot\). A closed tree is the outline of a derivation; an open branch is the countermodel.

A finite strict linear order has a first and a last instant and is not dense, so it can refute nothing in unbounded or dense time; and some formulas are refuted in \(K_l\) only by infinite orders, such as \(\neg(\mathbf{F}\top \land \mathbf{GF}\top)\), false at the start of the natural numbers. For linear time the prover therefore looks first for a strict finite countermodel and then, if there is none, for a finite linear order in which some instants are reflexive (\(w \prec w\)). Such an instant stands for a cluster: bulldozing (Segerberg [9], Burgess [10]) replaces every cluster by copies of the integers (of the rationals for dense time) and yields a strict linear order, with the same conditions, in which the same labeled formulas are true. This is also why Volpe needs no rule for irreflexivity. For instance, \(\mathbf{F}Q \to \mathbf{FF}Q\) is refuted in unbounded linear time by four points, with a cluster at each end (the integers after bulldozing):

W = {s, t, u, x}
< = {s < t, t < t, u < s, u < t, u < u, u < x, x < s, x < t}
V(Q) = {s}

Run it in SWI-Tinker

If no countermodel is found, the prover searches for a derivation in Volpe’s system, by iterative deepening. The introduction rules are applied backwards from the goal, the elimination rules forwards from the hypotheses (\(\mathbf{G}\)E and \(\mathbf{H}\)E along every available relation, \(\mathbf{F}\)E and \(\mathbf{P}\)E eagerly), and classical \(\bot\)E is the last resort. conn< is used to identify two instants that are not comparable, by transporting hypotheses from one to the other. trans<, ser and dens< are tried only when the goal or the hypotheses call for them, and the search is bounded in depth and in number of inferences. Every derivation found is checked by an independent checker: each rule application, each discharge, the freshness of every eigenlabel.

The derivations that Volpe gives in chapter 4 are part of the tests of the prover: the axioms KG and GP (proof of theorem 4.5), TRANS_R and CONN_R (theorem 4.7), SER_R and DENS_R (section 4.2.3), and their mirror images. The prover finds each of them with the same rules, in the same order, as in the thesis; each axiom is also refuted, by a checked countermodel, in the system without the rule it needs.

The countermodel tree is printed in ASCII and as LaTeX source for qtree; the derivation is printed as a tree (bussproofs) and in Fitch style (Klüwer’s fitch.sty, the package used by G4+), with the tense operators in bold. In SWI-Tinker, Ctrl-M renders the derivations; the trees are given as source, since MathJax has no qtree. Where a trans< step can be moved down the derivation, it is placed just above the rule that discharges its premisses.