{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,7]],"date-time":"2024-02-07T00:35:55Z","timestamp":1707266155626},"reference-count":15,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2022,9,5]],"date-time":"2022-09-05T00:00:00Z","timestamp":1662336000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,1,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic ${\\operatorname {CQC}}$ into Intuitionistic Predicate Logic ${\\operatorname {IQC}}$. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to ${\\operatorname {BQC}}$ of [12], a proper subsystem of ${\\operatorname {IQC}}$, go through as well. The obvious generalizations of Kuroda\u2019s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome the absence of full modus ponens in Basic Predicate Logic. In [3] we argued that ${\\operatorname {IQC}}$ is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, ${\\operatorname {BQC}}$. One concern is that ${\\operatorname {BQC}}$ is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns.<\/jats:p>","DOI":"10.1093\/jigpal\/jzac067","type":"journal-article","created":{"date-parts":[[2022,9,5]],"date-time":"2022-09-05T12:58:44Z","timestamp":1662382724000},"page":"47-63","source":"Crossref","is-referenced-by-count":0,"title":["Kolmogorov and Kuroda translations into basic predicate logic"],"prefix":"10.1093","volume":"32","author":[{"given":"Mohammad","family":"Ardeshir","sequence":"first","affiliation":[{"name":"Department of Mathematical Sciences, Sharif University of Technology , PO Box 11365-9415, Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wim","family":"Ruitenburg","sequence":"additional","affiliation":[{"name":"Department of Mathematical and Statistical Sciences, Marquette University , PO Box 1881, Milwaukee, WI 53201, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"key":"2024020618004173700_ref1","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1215\/00294527-3339473","article-title":"Boolean algebras in Visser algebras","volume":"57","author":"Alizadeh","year":"2016","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2024020618004173700_ref2","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1002\/malq.19980440304","article-title":"Basic propositional calculus I","volume":"44","author":"Ardeshir","year":"1998","journal-title":"Mathematical Logic Quarterly"},{"key":"2024020618004173700_ref3","article-title":"A constructive interpretation of the logical constants","author":"Ardeshir"},{"key":"2024020618004173700_ref4","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1007\/s00153-018-0656-x","article-title":"A Kuroda-style j-translation","volume":"58","author":"van den Berg","year":"2019","journal-title":"Archive for Mathematical Logic"},{"key":"2024020618004173700_ref5","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1017\/jsl.2013.10","article-title":"Glivenko and Kuroda for simple type theory","volume":"79","author":"Brown","year":"2014","journal-title":"The Journal of Symbolic Logic"},{"key":"2024020618004173700_ref6","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/067","volume-title":"Mathematical Intuitionism, Introduction to Proof Theory","author":"Dragalin","year":"1988"},{"key":"2024020618004173700_ref7","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0061811","article-title":"Lecture Notes in Mathematics 753","volume-title":"Applications of Sheaves","author":"Fourman","year":"1979"},{"key":"2024020618004173700_ref8","first-page":"183","article-title":"Sur quelques points de la logique de M. Brouwer","volume":"15","author":"Glivenko","year":"1929","journal-title":"Bulletins de la Classe des Sciences"},{"key":"2024020618004173700_ref9","first-page":"1879","article-title":"From Frege to G\u00f6del, A Source Book in Mathematical Logic","author":"van Heijenoort","year":"1967"},{"key":"2024020618004173700_ref10","first-page":"646","article-title":"O printsipe tertium non datur","volume-title":"Mathemati\u010deskii\u030c Sbornik 32","author":"Kolmogorov","year":"1925"},{"key":"2024020618004173700_ref11","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1017\/S0027763000010023","article-title":"Intuitionistische Untersuchungen der formalistischen Logik","volume":"2","author":"Kuroda","year":"1951","journal-title":"Nagoya Mathematical Journal"},{"key":"2024020618004173700_ref12","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1305\/ndjfl\/1039293019","article-title":"Basic predicate calculus","volume":"39","author":"Ruitenburg","year":"1998","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2024020618004173700_ref13","doi-asserted-by":"crossref","article-title":"Identity and existence in intuitionistic logic","author":"Scott","DOI":"10.1007\/BFb0061839"},{"key":"2024020618004173700_ref14","article-title":"Studies in Logic and the Foundations of Mathematics 121","volume-title":"Constructivism in Mathematics, an Introduction, Volume 1","author":"Troelstra","year":"1988"},{"key":"2024020618004173700_ref15","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF01874706","article-title":"A propositional logic with explicit fixed points","volume":"40","author":"Visser","year":"1981","journal-title":"Studia Logica"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/32\/1\/47\/56586549\/jzac067.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/32\/1\/47\/56586549\/jzac067.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,6]],"date-time":"2024-02-06T18:02:08Z","timestamp":1707242528000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/32\/1\/47\/6679414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,5]]},"references-count":15,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,9,5]]},"published-print":{"date-parts":[[2024,1,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzac067","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2024,2]]},"published":{"date-parts":[[2022,9,5]]}}}