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 <>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing this directive]