Reflexive intermediate propositional logics (Q2505130)

The author modifies the formulation and proof of a theorem due to \textit{D. C. McCarty} [Notre Dame J. Formal Logic 43, 243--248 (2002; Zbl 1050.03041)] to get the following statement: Let \(T\) be a second-order theory based on a superintuitionistic logic. If \(T\) proves the completeness theorem (consistency implies existence of a model) for some superintuitionistic propositional logic, then \(T\) proves every instance of \(\neg\varphi\vee\neg\neg\varphi\). The proof uses very few properties of \(T\) except comprehension. Defining \(A= \{p\mid\neg\varphi\}\cup \{\neg p\mid\neg\neg\varphi\}\) and \(B= A\cup\{p\vee\neg p\}\), \(B\) is consistent since both \(\{p\}\) and \(\{\neg p\}\) are. By completeness, there is a model \(M\models B\), hence \(M\models p\vee\neg p\), so \(\neg\varphi\vee\neg\neg\varphi\).