An Intermediate Logic Contained in Medvedev's Logic with Disjunction Property
Zhicheng Chen
TL;DR
This work identifies SU as a strong intermediate logic formed by adding the axiom $su$ to intuitionistic logic, situating it below Medvedev's logic ML but above KP and Scott logic, and proving two main results: (i) a precise frame correspondence where $su$ on $S\!4$ frames captures a strong union property, and (ii) that SU has the disjunction property and is Kripke complete with a canonical-model proof. The completeness shows SU is axiomatizable and exhibits the disjunction property, positioning SU as the strongest known logic beneath $ML$ with both axiomatization and DP. The combination advances understanding of Medvedev-frame-inspired logics and their Kripke semantics, with potential implications for constructive content in disjunctions and intermediate-logics between IPL and ML.
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.