Combining intermediate propositional logics with classical logic

TL;DR

This paper introduces an extended modal logic combining intermediate propositional logics with classical logic, providing Kripke semantics and a method to derive algebraic and Kripke completeness for various intermediate logics.

Contribution

It develops the logic $L5$ with Kripke semantics and generalizes to $L5(I)$ for intermediate logics, offering a new approach to completeness proofs and semantics determination.

Findings

$L5$ has Kripke semantics with added introspection

$L5(I)$ generalizes to various intermediate logics

Provides new proofs for classical intermediate logic completeness

Abstract

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\"odel-Dummett Logic and Jankov Logic. Our method provides new proofs of completeness theorems due to Hosoi, Dummett/Horn and Jankov, respectively.