Supplement to Temporal Logic

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.

Copyright © 2020 by
Valentin Goranko <>
Antje Rumberg <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free