Investigations on intuitionistic logic and modal logic

Abstract

Im Zuge der Diplomarbeit werden 3 nichtklassische Logiken betrachtet: intuitionistische Logik, Modallogik, die intuitionisische Modallogik HK[], die in "Milan Bozic und Kosta Dosen, Models for normal intuitionistic logics. Studia Logica, 43:217-245, 1984" zum ersten Mal vorgestellt wurde.<br />Der Korrektheits- und Vollständigkeitsbeweis für intuitionistische Logik erfolgt für die üblichen intuitionistischen Kripke-Modelle sowohl für ein Hilbert-Typ Kalkül als auch für ein Kalkül des natürlichen Schließens. Hier wird mittels eines Simulationsresultats der Korrektheits- und Vollständigkeitsbeweis für beide Systeme auf einmal erbracht.<br />Bei der Betrachtung von Modallogik wird die Korrektheit und Vollständigkeit der Logiken K, T, D, S4 und S5 formalisiert durch Hilbert-Typ Kalküle für die üblichen modalen Kripke Modelle vorgestellt.<br />Im Zuge der Untersuchungen der intuitionistischen Modallogik HK[] wurden einige schwere Lücken in der Beweisführung des Vollständigkeitsbeweises aufgezeigt. Ob HK[] überhaupt vollständig in Bezug zu den vorgestellten Kripke Modellen für intuitionistische Modallogik mit einem modalen operator [] ist, bleibt eine offene Frage.

In this thesis, we investigate three different non-classical propositional logics, which are relevant to computer science.<br />The first logic under consideration is intuitionistic logic. We present a Hilbert style calculus and a calculus of natural deduction, and show completeness and soundness for both of them with respect to intuitionistic Kripke models.<br />Then we investigate normal modal logic, with an emphasis on K, the basic normal modal logic. We also glimpse at stronger normal modal logics.<br />Here we only present one calculus, a Hilbert style calculus, extended to fit the new requirements to show completeness.<br />In the last part, we direct our attention to a relatively new non-classical logic; namely intuitionistic modal logic. We investigate the soundness and completeness of the system HK[], which was first presented in "Milan Bozic und Kosta Dosen, Models for normal intuitionistic logics. Studia Logica, 43:217-245, 1984". We identified some severe gaps in the completeness proof in this paper.