On an extension of Gabbay's logic (Q1972663)

The author considers the logic Gab obtained by adding to the intuitionistic logic Int the following four axioms: 1) \(p\rightarrow\varphi (p)\), 2) \(\varphi (p)\rightarrow\neg\neg p\), 3) \(\varphi (p)\rightarrow(q\vee (q\rightarrow p))\), 4) \((\varphi (p)\rightarrow p)\rightarrow (\neg\neg p\rightarrow p)\). This logic was treated by \textit{D. M. Gabbay} [Stud. Log. 36, No. 1-2, 127-139 (1977; Zbl 0363.02026)] as an example of a logic defining a new intuitionistic propositional connective. In the article under review, the logic Gab is studied from the point of view of Novikov's approach to intuitionistic connectives [see \textit{Ya. S. Smetanich}, Sov. Math., Dokl. 2, 937-939 (1961; Zbl 0122.00804)]. According to Novikov, a \(\varphi\)-logic \(L\), i.e., a logic in the language with an additional unary connective \(\varphi\), defines a new intuitionistic propositional connective whenever the following conditions hold: \(L\) is conservative over Int; \(L\) contains the axiom \((p\leftrightarrow q)\rightarrow (\varphi (p)\leftrightarrow\varphi (q))\); for every formula \(D\) in the language of Int, the \(\varphi\)-logic \(L+\varphi (p)\leftrightarrow D\) is not conservative over Int. A conservative \(\varphi\)-logic is Novikov complete if, for every formula \(A\notin L\), the \(\varphi\)-logic \(L+A\) is not conservative over Int. The author verifies that Gab meets the conditions of the above definition, i.e., Gab defines a new intuitionistic propositional connective in the sense of Novikov. Further, the class of generalized \(\varphi\)-frames is defined so that the \(\varphi\)-logic of this class extends Gab and is Novikov complete. The axiomatization problem for the logic constructed remains open.