A hierarchical completeness proof for propositional temporal logic

Abstract

We present a new proof of axiomatic completeness for Proposition Temporal Logic (PTL) for discrete, linear time for both finite and infinite time (without past-time). This makes use of a natural hierarchy of logics and notions and is an interesting alternative to the proofs in the literature based on tableaux, filtration, game theory and other methods. In particular we exploit the deductive completeness of a sublogic in which the only temporal operator is O ("next"). This yields a proof which is in certain respects more direct and higher-level than previous ones. The presentation also reveals unexpected fundamental links to a natural and preexisting framework for interval-based reasoning and fixpoints of temporal operators. © Springer-Verlag Berlin Heidelberg 2003.