An Intermediate Logic Contained in Medvedev's Logic with Disjunction Property

TL;DR

This paper introduces the superintuitionistic logic SU, which is contained in Medvedev's logic, has the disjunction property, and corresponds to a specific first-order property on S4 frames, establishing its strong completeness.

Contribution

It identifies the logic SU as the strongest known logic below Medvedev's logic with both an axiomatization and the disjunction property, and characterizes it via a first-order property on S4 frames.

Findings

SU is contained in Medvedev's logic

SU has the disjunction property

SU is strongly complete with respect to S4 frames with the strong union property

Abstract

Let $\textbf{SU}$ be the superintuitionistic logic defined by the axiom $\boldsymbol{su} = ((\neg p\to q)\land(\neg q\to p) \rightarrow r \vee s) \to ( p \rightarrow r) \vee(q \rightarrow s)$, or equivalently, by Andrew's axiom. It is easy to check that $\textbf{SU}$ is contained in Medvedev's logic and contains both Kreisel-Putnam logic and Scott logic. We show that on \textbf{S4} frames, $\boldsymbol{su}$ corresponds to a certain first-order property, called the ``strong union'' property. The strong completeness of \textbf{SU}, with respect to the class of \textbf{S4} frames enjoying this property, is proved. Furthermore, we demonstrate that \textbf{SU} has the disjunction property. As a result, \textbf{SU} stands as the strongest logic currently known below Medvedev's logic that has both an axiomatization and the disjunction property.