Supplement: Burgess-Xu Axiomatic System for Since and Until and Some Extensions

The axiomatic system of Burgess-Xu for the reflexive versions of \(S\) and \(U\) extends classical propositional logic with the following axiom schemata and their mirror images, with \(U\) and \(S\) as well as \(G\) and \(H\) swapped:

• \(G\varphi \rightarrow \varphi\)
• \(G(\varphi \rightarrow \psi)\rightarrow \varphi U\chi \rightarrow \psi U\chi\)
• \(G(\varphi \rightarrow \psi)\rightarrow \chi U\varphi \rightarrow \chi U\psi\)
• \(\varphi \wedge \chi U\psi \rightarrow \chi U(\psi \wedge \chi S\varphi)\)
• \(\varphi U\psi \rightarrow (\varphi \wedge \varphi U\psi)U\psi\)
• \(\varphi U(\varphi \wedge \varphi U\psi)\rightarrow \varphi U\psi\)
• \(\varphi U\psi \wedge \chi U\theta \rightarrow (\varphi \wedge \chi)U(\psi \wedge \theta)\vee (\varphi \wedge \chi)U(\psi \wedge \chi)\vee (\varphi \wedge \chi)U(\varphi \wedge \theta)\)

and the inference rules NEC\(_G\) and NEC\(_H\). This axiomatization, translated for the strict versions of \(S\) and \(U\), was extended by Venema (1993) to complete axiomatic systems for:

• all discrete linear orderings, by adding \(F\top \rightarrow \bot U\top\) and its dual \(P\top \rightarrow \bot S\top\);
• all well-orderings, by further adding \(H\bot \vee PH\bot\) and \(F\varphi \rightarrow (\lnot \varphi)U\varphi\);
• \(\left\langle \mathbf{N,\lt}\right\rangle\), by adding \(F\top\) to the previous system.