A new regular constant in intuitionistic propositional logic (Q1357985)

The author considers intuitionistic propositional logic where, besides the operations \(\&,\vee, \supset\), and \(\neg\), and besides the usual constants 0 and 1, there is an additional constant \(\varphi\). As models the author uses Kripke models. One such logic, denoted by Reg, is characterized through the following properties: 1) \(\neg\neg \varphi\) and \(\varphi\) are equivalent; 2) \(\varphi\vee\neg\varphi\) is the smallest \(\gamma\) for which \(\neg\gamma=0\). The intuitionistic deductive system is expanded for Reg and completeness of the expanded system is proved. For a further expansion of this logic, the author considers a special type of models, i.e., finite Kripke models whose last but one vertices are followed exactly by two last ones, forming in this way a forking, such that \(\varphi\) is valid exactly in one of the end vertices of each forking. The logic for these models is denoted by \(\text{Reg}^+\). The deductive system of Reg is extended for \(\text{Reg}^+\) and completeness of the extended system is proved.