Supplement to Temporal Logic

Supplement: Reynolds’ Axiomatic System for OBTL

Reynolds (2003) proposed complete axiomatic systems for OBTL for both bundled tree validity and Ockhamist validity, assuming instant-based atomic propositions. The former system extends the list of axioms and inference rules for \(G\) and \(H\) on linearly ordered time flows with the S5 axioms for \(\Box\), the axiom \(G \bot \to \Box G \bot\) implying maximality of histories, the axiom scheme

  • (HN) \(P \varphi \to \Box P \Diamond \varphi\),

saying that all histories through the current instant share the same past, and the so-called Gabbay Irreflexivity Rule, used to force irreflexivity of the temporal precedence relation:

  • (IRR) If \(\vdash (p\land H \lnot p) \to \varphi\), then \(\vdash \varphi\), provided \(p\) does not occur in \(\varphi\).

In order to completely axiomatize Ockhamist validity, Reynolds adds the following infinite scheme of “limit closure axioms”:

  • (LC) \(\Box G_{\leq} \bigwedge_{i=0}^{n-1} (\Diamond \varphi_{i} \to \Diamond F \Diamond \varphi_{i+1}) \to \Diamond G_{\leq} \bigwedge_{i=0}^{n-1} (\Diamond \varphi_{i} \to F \Diamond \varphi_{i+1})\)

where \(\varphi_{0},\ldots, \varphi_{n-1}\) are any OBTL formulae, \(\varphi_{n} = \varphi_{0}\), and \(G_{\leq} \theta := \theta \land G\theta\).

Copyright © 2020 by
Valentin Goranko <>
Antje Rumberg <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free