A Full-Circle Theorem for Simple Tense Logic

A full-circle theorem 1 for a given logical system ℒ says that certain proof systems S 1, ..., S 4 for ℒ of the four most important types of inference systems (Hilbert-style, natural deduction, tableaux, sequent calculi) are all equivalent in the following sense (cf. Figure 1): Every proof of a wff A from wffs A 1,..., A k in S 1 can be transformed into a proof of A from A 1,..., A k in S 2; every proof of A from A 1,..., A n in S 4 can be transformed into a proof of A from A 1,..., A k in S 1.