A Kuroda-style j-translation

Subsystems of classical logic (including intuitionistic logic) (03B20) Relative consistency and interpretations (03F25) Metamathematics of constructive systems (03F50)

Abstract: In topos theory it is well-known that any nucleus j gives rise to a translation of intuitionistic logic into itself in a way which generalises the Goedel-Gentzen negative translation. Here we show that there exists a similar j-translation which is more in the spirit of Kuroda's negative translation. The key is to apply the nucleus not only to the entire formula and universally quantified subformulas, but to conclusions of implications as well. The development is entirely syntactic and no knowledge of topos theory is required to read this small note.

Review text

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)].

Recommendations

Cited in

(7)

This page was built for publication: A Kuroda-style \(j\)-translation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2312092)