A Full-Circle Theorem for Simple Tense Logic

Abstract

A full-circle theorem ¹ for a given logical system ℒ says that certain proof systems S ₁, ..., S ₄ 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 ₁,..., A _k in S ₁ can be transformed into a proof of A from A ₁,..., A _k in S ₂;

• every proof of A from A ₁,..., A _n in S ₄ can be transformed into a proof of A from A ₁,..., A _k in S ₁.