Abstract
Proof theory of modal logics, though largely studied since the fifties, has always been a delicate subject, the main reason being the apparent impossibility to obtain elegant, natural systems for intensional operators (with the excellent exception of intuitionistic logic). For example Segerberg, not earlier than 1984 [5], observed that the Gentzen format, which works so well for truth functional and intuitionistic operators, cannot be a priori expected to remain valid for modal logics; carrying to the limit this observation one could even assert that ‘logics with no good proof theory are unnatural.’ In such a way we should mark as ‘unnatural’ all modal logics (with great delight of a large number of logicians!).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
H. Barendregt. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Revised Edition.
H. Barendregt. Lambda calculus with types. In: S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, (eds.), Handbook of Logic in Computer Science, Vol. II Background: Computational Structures, pp. 118–310. Oxford University Press, 1992.
M. R. F. Benevides, T. S. E. Maibaum. A constructive presentation for the modal connective of necessity (0). Journal of Logic and Computation, 2, 31–50, 1992.
G. Bierman, C. Mere, V. de Paiva. Intuitionistic necessity revisited. In: Logic at Work: Applied Logic Conference, 1992.
R. Bull, K. Segerberg. Basic modal logic. In: D. Gabbay, F. Guenthner, (eds.), Handbook of Philosophical Logic, Vol. II, pp. 1–88. Reidel, 1984.
K. Dolen. Sequent-systems for modal logic. Journal of Symbolic Logic, 50, 149–168, 1985.
D. M. Gabbay, R. J.G.B. de Queiroz. Extending the Curry-Howard interpretation to linear, relevant and other resource logics. Journal of Symbolic Logic, 57, 1319–1365, 1992.
D. M. Gabbay, R. J.G.B. de Queiroz. An introduction to labelled natural deduction. Proceedings of Third Advanced Summer School in Artificial Intelligence, 1992.
J.-Y. Girard. Proof Theory and Logical Complexity. Bibliopolis, 1987.
S. Kripke. Semantical analysis of modal logic I. Zeitschr f. math. Logik and Grund. d. Mathematik, 9, 67–96, 1963.
A. Masini. 2-Sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58, 229–246, 1992.
A. Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of - Log ic and Computation, 3, 533–562, 1993.
G. Mints. Selected Papers in Proof Theory. Bibliopolis, 1992.
D. Prawitz. Natural Deduction. Acta Universitatis Stockholmiensis, Stockholm Studies in Philosophy 3, Almqvist & Wiksell, Stockholm, 1965.
A. S. Troelstra. Natural deduction for intuitionistic linear logic. Annals of Pure and Applied Logic, 73, 79–108, 1995.
A. S. Troelstra and Dirk van Dalen. Constructivism in Mathematics, Vol. II. North-Holland, 1988.
H. Wansing. Sequent calculi for normal modal propositional logic. Journal of Logic and Computation, 4, 125–142, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Martini, S., Masini, A. (1996). A Computational Interpretation of Modal Proofs. In: Wansing, H. (eds) Proof Theory of Modal Logic. Applied Logic Series, vol 2. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-2798-3_12
Download citation
DOI: https://doi.org/10.1007/978-94-017-2798-3_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-4720-5
Online ISBN: 978-94-017-2798-3
eBook Packages: Springer Book Archive