Yes, of course you can. But most proof systems for temporal logics (including the one in the slides that you pointed to) are Hilbert-style systems that are not exactly easy to use in practice. If you are lucky, temporal logic books show by induction that you can provably substitute a subformula for an equivalent one and then appeal to this lemma in later proofs. However, one nice aspect of propositional temporal logic (PTL) is that it is decidable. So, you could use some decision procedure for PTL such as ls4 (http://www.cs.man.ac.uk/~sudam/, the system that we use in the TLA+ Proof System) and ask it if the formula [](P <=> Q) /\ [](R <=> S) => []( (P until R) <=> (Q until S) ) is valid, and it will tell you that it is. The validity of this formula is equivalent to the validity of your sequent.
First-order temporal logic is easy to define semantically, but hard to axiomatize. In fact, it is expressive enough to unambiguously define arithmetic with addition and multiplication over the natural numbers and any formal axiom system must therefore be incomplete, by Gödel's incompleteness theorem. So logicians find first-order temporal logic mostly boring, unless they can find a fragment with nice meta-properties such as decidability. For deductive program verification, you cannot avoid it but only use a few basic axioms such as (\A x : []F(x)) <=> [](\A x : F(x)) and a rule for proving liveness from well-founded orderings such as (S, <) is well-founded ----------------------------------------------------------------------------------------------------- (\A x \in S : F(x) ~> (G \/ \E y \in S : y < x /\ F(y)) => ((\E x \in S : F(x)) ~> G) Best regards, Stephan |