On the proof-theory of two formalisations of modal first-order logic (Q622627)

Tourlakis and Kibedi introduced some modal first-order logics for a modal interpretation of the provability of classical logic. In this paper, a Gentzen-style sequential calculus is provided for them, and shown to enjoy the cut-elimination property. The modal logics, which have been given in a Hilbert-style axiomatization, are shown to be translatable into the Gentzen system (repspectively in different ways), so that the results obtained model-theoretically in the former works are reconstructed by proof-theoretical means. It is also proved that the form of ``weak reflection'', one of the results thus obtained, is as strong as possible.