## 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$$.