Let SU be the superintuitionistic logic defined by the axiom <InlineEquation ID="IEq1"> <EquationSource Format="TEX">$\varvec{su} = ((\lnot p\rightarrow q)\wedge (\lnot q\rightarrow p) \rightarrow r \vee s) \rightarrow ( p \rightarrow r) \vee (q \rightarrow s)$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mrow> <mi mathvariant="bold-italic">su</mi> </mrow> <mo>=</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mo>¬</mo> <mi>p</mi> <mo stretchy="false">→</mo> <mi>q</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mo>¬</mo> <mi>q</mi> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>r</mi> <mo>∨</mo> <mi>s</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>p</mi> <mo stretchy="false">→</mo> <mi>r</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi>q</mi> <mo stretchy="false">→</mo> <mi>s</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation>, or equivalently, by Andrew’s axiom. It is easy to check that SU is contained in Medvedev’s logic and contains both Kreisel-Putnam logic and Scott logic. We show that on intuitionistic frames, <InlineEquation ID="IEq2"> <EquationSource Format="TEX">$\varvec{su}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="bold-italic">su</mi> </mrow> </math></EquationSource> </InlineEquation> corresponds to a certain first-order property, called the “strong union” property. The strong completeness of SU, with respect to the class of intuitionistic frames enjoying this property, is proved. Furthermore, we demonstrate that SU has the disjunction property. To the best of our knowledge, SU is the strongest logic currently known below Medvedev’s logic that has both a finite axiomatization and the disjunction property.

An Intermediate Logic Contained in Medvedev’s Logic with the Disjunction Property

期刊论文
发表日期：

2026年5月16日

查看全文

Zhicheng Chen

摘要

Let SU be the superintuitionistic logic defined by the axiom $\varvec{su} = ((\lnot p\rightarrow q)\wedge (\lnot q\rightarrow p) \rightarrow r \vee s) \rightarrow ( p \rightarrow r) \vee (q \rightarrow s)$ $su = ((\neg p \to q) \land (\neg q \to p) \to r \lor s) \to (p \to r) \lor (q \to s)$ , or equivalently, by Andrew’s axiom. It is easy to check that SU is contained in Medvedev’s logic and contains both Kreisel-Putnam logic and Scott logic. We show that on intuitionistic frames, $\varvec{su}$ $su$ corresponds to a certain first-order property, called the “strong union” property. The strong completeness of SU, with respect to the class of intuitionistic frames enjoying this property, is proved. Furthermore, we demonstrate that SU has the disjunction property. To the best of our knowledge, SU is the strongest logic currently known below Medvedev’s logic that has both a finite axiomatization and the disjunction property.