{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T14:33:42Z","timestamp":1758810822083},"reference-count":34,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Intuitionistic epistemic logic introduces an epistemic operator to intuitionistic logic, which reflects the intended Brouwer\u2013Heyting\u2013Kolmogorov (BHK) semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the logic of proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, providing the systems of intuitionistic epistemic logic based on verification with an arithmetical semantics too. This confirms that the conception of verification incorporated in these systems reflects the BHK interpretation.<\/jats:p>","DOI":"10.1093\/logcom\/exaa016","type":"journal-article","created":{"date-parts":[[2020,1,7]],"date-time":"2020-01-07T06:00:24Z","timestamp":1578376824000},"page":"381-402","source":"Crossref","is-referenced-by-count":1,"title":["An arithmetic interpretation of intuitionistic verification"],"prefix":"10.1093","volume":"30","author":[{"given":"Tudor","family":"Protopopescu","sequence":"first","affiliation":[{"name":"Borough of Manhattan Community College, City University of New York, New York City, NY 10007, USA"}]}],"member":"286","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"key":"2020040702452104700_ref1","article-title":"Operational modal logic","volume-title":"Technical Report MSI 95-29","author":"Artemov","year":"1995"},{"key":"2020040702452104700_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","article-title":"Explicit provability and constructive semantics","volume":"7","author":"Artemov","year":"2001","journal-title":"Bulletin of Symbolic Logic"},{"key":"2020040702452104700_ref3","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1017\/S1755020308090060","article-title":"The logic of justification","volume":"1","author":"Artemov","year":"2008","journal-title":"Review of Symbolic Logic"},{"key":"2020040702452104700_ref4","first-page":"125","article-title":"Constructive knowledge and the justified true belief paradigm","volume-title":"Indagationes Mathematicae","author":"Artemov","year":"2018"},{"article-title":"The provability of consistency","year":"2019","author":"Artemov","key":"2020040702452104700_ref5"},{"key":"2020040702452104700_ref6","first-page":"189","article-title":"Provability logic","volume-title":"Handbook of Philosophical Logic","author":"Artemov","year":"2005"},{"key":"2020040702452104700_ref7","doi-asserted-by":"crossref","DOI":"10.1017\/9781108348034","volume-title":"Justification Logic: Reasoning with Reasons. Cambridge Tracts in Mathematics 216","author":"Artemov","year":"2019"},{"key":"2020040702452104700_ref8","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.1093\/logcom\/exi053","article-title":"Introducing justification into epistemic logic","volume":"15","author":"Artemov","year":"2005","journal-title":"Journal of Logic and Computation"},{"key":"2020040702452104700_ref9","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1017\/S1755020315000374","article-title":"Intuitionistic epistemic logic","volume":"9","author":"Artemov","year":"2016","journal-title":"Review of Symbolic Logic"},{"volume-title":"The Logic of Provability","year":"1993","author":"Boolos","key":"2020040702452104700_ref10"},{"key":"2020040702452104700_ref11","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.tcs.2006.03.010","article-title":"Making knowledge explicit: how hard it is","volume":"357","author":"Brezhnev","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"2020040702452104700_ref12","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"Chagrov","year":"1997"},{"key":"2020040702452104700_ref13","doi-asserted-by":"crossref","DOI":"10.4064\/fm-49-1-35-92","article-title":"Arithmetization of metamathematics in a general setting","volume":"49","author":"Feferman","year":"1960","journal-title":"Fundamenta Mathematicae"},{"key":"2020040702452104700_ref14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.apal.2004.04.009","article-title":"The logic of proofs. Semantically","volume":"132","author":"Fitting","year":"2005","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702452104700_ref15","first-page":"615","article-title":"Modal logics, justification logics and realization","volume-title":"Annals of Pure and Applied Logic","author":"Fitting","year":"2016"},{"key":"2020040702452104700_ref16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-54332-0_17","article-title":"Quasi-realization","volume-title":"Logic, Language, and Computation","author":"Fitting","year":"2017"},{"key":"2020040702452104700_ref17","first-page":"301","article-title":"An interpretation of the intuitionistic propositional calculus","volume-title":"Collected Works","author":"G\u00f6del","year":"1933"},{"key":"2020040702452104700_ref18","first-page":"42","article-title":"The intuitionistic foundations of mathematics","volume-title":"Philosophy of Mathematics, Selected Readings","author":"Heyting","year":"1964"},{"volume-title":"Intuitionism: An Introduction","year":"1971","author":"Heyting","key":"2020040702452104700_ref19"},{"key":"2020040702452104700_ref20","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-642-17511-4_16","article-title":"An intuitionistic epistemic logic for sequential consistency on shared memory","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Hirai","year":"2010"},{"key":"2020040702452104700_ref21","first-page":"420","article-title":"A canonical model construction for intuitionistic distributed knowledge","volume-title":"Advances in Modal Logic","author":"J\u00e1ger","year":"2016"},{"key":"2020040702452104700_ref22","first-page":"328","article-title":"On the interpretation of intuitionistic logic","volume-title":"From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920\u2019s","author":"Kolmogorov","year":"1932"},{"key":"2020040702452104700_ref23","article-title":"On modeling knowledge in social networks","volume-title":"Tenth Smirnov Readings in Logic","author":"Krupski","year":"2017"},{"key":"2020040702452104700_ref24","first-page":"187","article-title":"Sequent calculus for intuitionistic epistemic logic IEL","volume-title":"Logical Foundations of Computer Science. International Symposium. Proceedings. Logical Foundations of Computer Science. LFCS 2016 (Dearfield Beach, Florida, USA, Jan. 4\u20136, 2016)","author":"Krupski","year":"2016"},{"key":"2020040702452104700_ref25","doi-asserted-by":"crossref","DOI":"10.1093\/jigpal\/jzw002","article-title":"Weak arithmetical interpretations for the logic of proofs","author":"Kuznets","year":"2016","journal-title":"Logic Journal of the IGPL"},{"key":"2020040702452104700_ref26","article-title":"Mathematical Logic and Foundations","volume-title":"Logics of Proofs and Justifications","author":"Kuznets","year":"2019"},{"key":"2020040702452104700_ref27","first-page":"309","article-title":"Epistemic extensions of combined classical and intuitionistic propositional logic","volume-title":"Logic Journal of the IGPL","author":"Lewitzka","year":"2017"},{"key":"2020040702452104700_ref28","first-page":"218","article-title":"Reasoning about proof and knowledge","volume-title":"Annals of Pure and Applied Logic","author":"Lewitzka"},{"key":"2020040702452104700_ref29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268135","article-title":"Some theorems about the sentential calculi of Lewis and Heyting","volume":"13","author":"McKinsey","year":"1948","journal-title":"The Journal of Symbolic Logic"},{"key":"2020040702452104700_ref30","doi-asserted-by":"crossref","first-page":"877","DOI":"10.1007\/s10992-011-9207-1","article-title":"Intuitionistic epistemic logic, Kripke models and Fitch\u2019s paradox","volume":"41","author":"Proietti","year":"2012","journal-title":"Journal of Philosophical Logic"},{"key":"2020040702452104700_ref31","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-662-48561-3_24","article-title":"Intuitionistic epistemology and modal logics of verification","volume-title":"Proceedings. Logics, Rationality and Interaction (LORI 2015). (Oct. 26\u201329, 2015)","author":"Protopopescu","year":"2015"},{"key":"2020040702452104700_ref32","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/978-3-662-60292-8_24","article-title":"First- order intuitionistic epistemic logic","volume-title":"Logic, Rationality, and Interaction","author":"Su","year":"2019"},{"key":"2020040702452104700_ref33","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2020040702452104700_ref34","first-page":"63","article-title":"On intuitionistic modal epistemic logic","volume":"21","author":"Williamson","year":"1992","journal-title":"Journal of Philosophical Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/381\/33016432\/exaa016.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/381\/33016432\/exaa016.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,29]],"date-time":"2024-07-29T20:28:35Z","timestamp":1722284915000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/381\/5739321"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":34,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,2,20]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa016","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}