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

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.