Bergen Logic Group

New publication: Bergen Logic Group

Tore Fjetland Øgaard | From Hilbert Proofs to Consecutions and Back | Australasian Journal of Logic

Main content

From Hilbert Proofs to Consecutions and Back

Tore Fjetland Øgaard


Restall set forth a "consecution" calculus in his An Introduction to Substructural Logics. This is a natural deduction type sequent calculus where the structural rules play an important role.  This paper looks at different ways of extending Restall's calculus. It is shown that Restall's weak soundness and completeness result with regards to a Hilbert calculus can be extended to a strong one so as to encompass what Restall calls proofs from assumptions. It is also shown how to extend the calculus so as to validate the metainferential rule of reasoning by cases, as well as certain theory-dependent rules.

KEYWORDS: consecution, external consequence, Hilbert consequence, relevant logic, substructural proof theory