A Kuroda-style \(j\)-translation (Q2312092)

Let \(\mathsf L\) be one of: \begin{itemize} \item classical predicate logic \(\mathsf{CQC}\); \item intuitionistic predicate logic \(\mathsf{IQC}\); \item minimal predicate logic \(\mathsf{MQC}\). \end{itemize} A nucleous is a mapping \(j\) of formulas that is \begin{itemize} \item monotone (that is \(\vdash_\mathsf L (\varphi \rightarrow \psi) \rightarrow (j\varphi \rightarrow j\psi)\)); \item inflationary (that is \(\vdash_\mathsf L \varphi \rightarrow j\varphi\)); \item idempotent (that is \(\vdash_\mathsf L j\varphi \leftrightarrow jj\varphi\)); \item commutes with conjunction (that is \(\vdash_\mathsf L j(\varphi \wedge \psi) \leftrightarrow (j\varphi \wedge j\psi)\)); \item commutes with substitution (that is \(\vdash_\mathsf L (j\varphi)[t/x] \leftrightarrow j(\varphi[t/x])\)); \item does not add free variables (that is \(\mathrm{FV}(j\varphi) \subseteq \mathrm{FV}(\varphi)\)). \end{itemize} Let \(A\) be a fixed sentence; some examples of nuclei are \begin{itemize} \item \(j\varphi \, = \, \neg\neg\varphi\); \item \(j\varphi \, = \, (\varphi \rightarrow A) \rightarrow A\); \item \(j\varphi \, = \, \varphi \vee A\); \item \(j\varphi \, = \, A \rightarrow \varphi\); \item \(j\varphi \, = \, (\varphi \rightarrow A) \rightarrow \varphi\). \end{itemize} If \(\Phi\) is a list of formulas \(\varphi_1,\ldots,\varphi_n\), then let \(\Phi^j\) be \(\varphi_1^j,\ldots,\varphi_n^j\); by applying a nucleous~\(j\) to \begin{itemize} \item atomic formulas (that is \(\varphi_\mathrm{at} \ \leadsto \ j\varphi_\mathrm{at}\)); \item disjunctions (that is \(\varphi \vee \psi \ \leadsto \ j(\varphi \vee \psi)\)); \item existential quantifiers (that is \(\exists x \, \varphi \ \leadsto \ j\exists x \, \varphi\)); \end{itemize} we get a translation~\(\cdot^j\) from \(\mathsf L\) to itself (that is \(\Phi \vdash_\mathsf L \psi \ \Rightarrow \ \Phi^j \vdash_\mathsf L \psi^j\)). For certain choices of nuclei, \(\cdot^j\) is a translation from \(\mathsf{CQC}\) to \(\mathsf{IQC}\) (that is \(\Phi \vdash_\mathsf{CQC} \psi \ \Rightarrow \ \Phi^j \vdash_\mathsf{IQC} \psi^j\)) or even to \(\mathsf{MQC}\) (that is \(\Phi \vdash_\mathsf{CQC} \psi \ \Rightarrow \ \Phi^j \vdash_\mathsf{MQC} \psi^j\)); translations of this type are know as negative translations. The translation~\(\cdot^j\) resembles the Gödel-Gentzen negative translation. The author proposes to apply the nucleous~\(j\) to \begin{itemize} \item the consequent of implications (that is \((\varphi \rightarrow \psi) \ \leadsto \ (\varphi \rightarrow j\psi)\)); \item universal quantifiers (that is \(\forall x \, \varphi \ \leadsto \ \forall x \, j\varphi\)); \end{itemize} getting a new \(j\)-translation~\(\cdot_j\) from \(\mathsf L\) to itself (that is \(\Phi \vdash_\mathsf L \psi \ \Rightarrow \ \Phi_j \vdash_\mathsf L j\psi_j\)). The author proves that for certain choices of nuclei, \(\cdot_j\) is a translation from \(\mathsf{CQC}\) to \(\mathsf{IQC}\) (that is \(\Phi \vdash_\mathsf{CQC} \psi \ \Rightarrow \ \Phi_j \vdash_\mathsf{IQC} j\psi_j\)) or even to \(\mathsf{MQC}\) (that is \(\Phi \vdash_\mathsf{CQC} \psi \ \Rightarrow \ \Phi_j \vdash_\mathsf{MQC} j\psi_j\)). The translation~\(\cdot_j\) resembles the Kuroda negative translation. As applications, the author recovers as corollaries to his translation~\(\cdot_j\) two results: \begin{itemize} \item if \(\varphi\) and \(\psi\) are formulas without \(\forall\) and \(\rightarrow\), then \(\varphi \vdash_\mathsf{CQC} \psi \ \Rightarrow \ \varphi \vdash_\mathsf{IQC} \psi\); \item if \(\psi\) is obtained from \(\varphi\) by replacing implications~\(\alpha \rightarrow \beta\) by \(\alpha \rightarrow (\beta \vee \bot)\) and universal quantifications~\(\forall x \, \alpha\) by \(\forall x \, (\alpha \vee \bot)\), then \(\vdash_\mathsf{IQC} \varphi \ \Rightarrow \ \; \vdash_\mathsf{MQC} \psi\). \end{itemize} Finally, he relates his translation~\(\cdot_j\) to \textit{M. J. Beeson}'s presentation of forcing [Foundations of constructive mathematics. Metamathematical studies. Berlin etc.: Springer-Verlag (1985; Zbl 0565.03028)].