Abstract
A nucleus is an operation on the collection of truth values which, like double negation in intuitionistic logic, is monotone, inflationary, idempotent and commutes with conjunction. Any nucleus determines a proof-theoretic translation of intuitionistic logic into itself by applying it to atomic formulas, disjunctions and existentially quantified subformulas, as in the Gödel–Gentzen negative translation. Here we show that there exists a similar translation of intuitionistic logic into itself 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.
Article PDF
Similar content being viewed by others
References
Aczel, P.: The Russell–Prawitz modality. Math. Struct. Comput. Sci. 11(4), 541–554 (2001). (Modalities in type theory (Trento, 1999))
Avigad, J.: Forcing in proof theory. Bull. Symb. Log. 10(3), 305–333 (2004)
Beeson, M.J.: Foundations of Constructive Mathematics, Volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)], Metamathematical studies. Springer, Berlin (1985)
Benton, P.N., Bierman, G.M., de Paiva, V.C.V.: Computational types from a logical perspective. J. Funct. Program. 8(2), 177–193 (1998)
Cohen, P.J.: Set Theory and the Continuum Hypothesis. W. A. Benjamin Inc, New York, Amsterdam (1966)
Colacito, A., de Jongh, D., Vargas, A.L.: Subminimal negation. Soft Comput. 21(1), 165–174 (2017)
Escardó, M., Oliva, P.: The Peirce translation. Ann. Pure Appl. Log. 163(6), 681–692 (2012)
Fairtlough, M., Mendler, M.: Propositional lax logic. Inf. Comput. 137(1), 1–33 (1997)
Ferreira, G., Oliva, P.: On the relation between various negative translations. In: Logic, Construction, Computation, Volume 3 of Ontos Mathematical Logic, pp. 227–258. Ontos Verlag, Heusenstamm (2012)
Johnstone, P.T.: Stone Spaces, Volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge (1982)
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Volume 43 of Oxford Logic Guides. Oxford University Press, The Clarendon Press, New York (2002)
Kuroda, S.: Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Math. J. 2, 35–47 (1951)
Lawvere, F.W.: Quantifiers and sheaves. In: Actes du CongrèsInternational des Mathématiciens (Nice, 1970), Tome 1, pp 329–334. Gauthier-Villars, Paris (1971)
Lee, S., van Oosten, J.: Basic subtoposes of the effective topos. Ann. Pure Appl. Log. 164(9), 866–883 (2013)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Universitext. Springer, New York (1994) (Corrected reprint of the 1992 edition)
Murthy, C.: Extracting Constructive Content from Classical Proofs. Ph.D. thesis, Cornell University, Department of Computer Science (1990). (TR 90-1151)
van der Molen, T.: The Johansson/Heyting letters and the birth of minimal logic. ILLC Publications, Technical Notes. http://www.illc.uva.nl/Research/Publications/Reports/X-2016-04.text.pdf (2016)
Acknowledgements
The author wishes to thank the referee for useful comments and Tomoaki Hashizaki, Taichi Uemura and Albert Visser for spotting errors in earlier versions.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
van den Berg, B. A Kuroda-style j-translation. Arch. Math. Logic 58, 627–634 (2019). https://doi.org/10.1007/s00153-018-0656-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-018-0656-x