Reduction of logics to the primitive logic
Katuzi Ono · Journal of the Mathematical Society of Japan · 1967
Faithful interpretation of the intuitionistic logic LJ and the classical logic LK in the primitive logic LO can be realized by $\mathfrak{R}$ -transform $\mathfrak{A}^{[\Re]}$ of any pro- position $\mathfrak{A}$ with respect to an n-ary relation R. $\mathfrak{A}^{[\Re]}$ can be defined recursively as follows ( $\xi$ stands for a sequence of $n$ distinct variables, none of them is assumed to occur free in $\mathfrak{F}$ and $\mathfrak{G}$ ):$\mathfrak{F}^{[\Re]}\equiv(\xi)((\mathfrak{F}\rightarrow \mathfrak{R}(\xi))\rightarrow \mathfrak{R}(\xi))$ for any elementary formula $\mathfrak{F}$ ,Now, we can prove the following theorem: $\mathfrak{A}$ is provable in LJ if and only if $\mathfrak{A}^{[R]}$ is provable in LO, assuming that $R$ is an n-ary relation symbol having no occurrence in $\mathfrak{A}$ for some $n(n\geqq 1)$ .$\mathfrak{A}$ is provable in LK if and only if $\mathfrak{A}^{[R]}$ is provable in LO, assuming that $R$ is $a$ O-ary relation symbol $i$ .$e$ .pro- position symbol having no occurrence in $\mathfrak{A}$ .