Appendix

Abstract

Many important logical systems have proof-theoretic presentations of more than one type, say, an axiomatization, a natural deduction proof system, and a sequent calculus presentation. Usually, this is a rather fortunate situation. It may happen that certain axiom schemata are characterizable by algebraic or relational properties expressible in an interesting fragment of first-order logic, and that Gentzen-style proof systems lend themselves to automated deduction. As we have seen, display logic is an elegant and powerful refinement of Gentzen’s sequent calculus and meets quite a few methodological requirements of a more philosophical and a more technical nature. It would be nice to relate the modal display calculus to natural deduction proof systems for intensional logics, and in the present chapter we shall relate DL to generalized Fitch-style natural deduction systems for modal logics. Moreover, we shall show that DL may have repercussions on the axiomatic presentation of logical systems and define an apparently new axiomatization of Kt. Eventually, we shall consider a generalization of DL, namely four-place display sequents. We shall redisplay Nelson’s system N4 and obtain a display sequent calculus for N3 by the addition of a purely structural sequent rule.