2015/10/19 by Steffen Lewitzka, Lewitzka, Steffen
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1510.05326
openalex publication_date 2015/10/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In [17], we introduced a modal logic, called L, which combines intuitionistic propositional logic IPC and classical propositional logic CPC and is complete w.r.t. an algebraic semantics. However, L seems to be too weak for Kripke-style semantics. In this paper, we add positive and negative introspection and show that the resulting logic L5 has a Kripke semantics. For intermediate logics I, we consider the parametrized versions L5(I) of L5 where IPC is replaced by I. L5(I) can be seen as a classical modal logic for the reasoning about truth in I. From our results, we derive a simple method for determining algebraic and Kripke semantics for some specific intermediate logics. We discuss some examples which are of interest for Computer Science, namely the Logic of Here-and-There, Gödel-Dummett Logic and Jankov Logic. Our method provides new proofs of completeness theorems due to Hosoi, Dummett/Horn and Jankov, respectively.