Supplement: Reynolds’ Axiomatic System for OBTL

Reynolds (2003) proposed complete axiomatic systems for OBTL, both for bundled tree validity and Ockhamist validity, assuming instant-based atomic propositions.

His system for bundled tree validity extends the minimal temporal logic \(\mathbf{K}_{t}\) (see Section 3.5) by the axiom schemata (TRANS), (LIN-F), and (LIN-P) (see Section 3.6) as well as

• the \(\mathbf{S5}\) axiom schemata for \(\Box\) (i.e. \(\Box(\varphi \rightarrow \psi) \rightarrow (\Box\varphi \rightarrow \Box\psi), \Box\varphi \rightarrow \varphi, \Diamond\varphi \rightarrow \Box\Diamond\varphi\)),
• the axiom scheme \(G \bot \to \Box G \bot\) for maximality of histories,
• the interaction axiom scheme \(P \varphi \rightarrow \Box P \Diamond \varphi\), and
• the axiom scheme \(p \rightarrow \Box p\) for instant-based atomic propositions.

The inference rules comprise, in addition to (MP), (NEC\(_H\)), and (NEC\(_G\)) (see Section 3.5),

• the necessitation rule for \(\Box\), and
• the so-called Gabbay Irreflexivity Rule: If \(\vdash (p\land H \lnot p) \to \varphi,\) then \(\vdash \varphi,\) provided \(p\) does not occur in \(\varphi\).

To completely axiomatize Ockhamist validity, Reynolds proposed to add the following infinite axiom scheme, which is supposed to guarantee the “limit closure property”:

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