Indexed systems of sequents and cut-elimination
Tóm tắt
Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cut-elimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations of the systems considered can be presented as encodings of Kripke-style formulations.
Tài liệu tham khảo
Belnap, N. (1982): Display logic, Journal of Philosophical Logic 11: 375–417.
Gentzen, G. (1934): Untersuchungen über das logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431.
Fitting, M. (1983): Proof Methods for Modal and Intuitionistic Logics, D. Reidel, Dordrecht.
Kleene, S. C. (1952): Introduction to Metamathematics, Amsterdam, North-Holland.
Kleene, S. C. (1952): Two papers on the predicate calculus, Memoirs of the American Mathematical Society 10: 1–66.
Kripke, S. (1963): Semantical analysis of modal logic I, Zeitschr. f. math. Logik und Grundl. d. Mathematik 9: 67–96.
Kripke, S. (1965): Semantical analysis of intuitionistic logic I. In: Formal Systems and Recursive Functions, North-Holland, Amsterdam, pp. 92–130.
Hughes, G. and Kresswell, M. (1972): An Introduction to Modal Logic, Methuen, The Hague.
Mints, G. (1992): A Short Introduction to Modal Logic. Center for the Study of Language and Information, Stanford, 91 p.
Mints, G. (1992): Selected Papers in Proof Theory, Bibliopolis, Napoli, Italia and North-Holland, Amsterdam.
Mints, G. (1971): On some calculi of modal logic. Proc. Steklov Inst. of Mathematics 98: 97–122.
Mints, G. (1992): Lewis systems and the system T. In: Mints, G. Selected Papers in Proof Theory. North-Holland-Bibliopolis, pp. 221–294 (Russian Original 1974).
Mints, G. (1983): Review of Belnap 1982. Referativnyi Zhurnal Matematika, 5A64.
Ohlbach, H. (1991): Semantic-based translation methods for modal logics, J. Logic and Computation 1(5): 691–746.
Wallen, L. (1990): Automated Deduction in Non-classical Logics, MIT Press, Cambridge, Mass.
Wansing, H. (1994): Modal calculi for normal modal propositional logics, J. Logic and Computation 4(2): 125–142.