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\).