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

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