{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T09:15:55Z","timestamp":1712222155842},"reference-count":55,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2020,10,2]],"date-time":"2020-10-02T00:00:00Z","timestamp":1601596800000},"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,12,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Nelson\u2019s logic of constructible falsity \u00a0$\\textsf{N}$ and Rauszer\u2019s Heyting\u2013Brouwer logic \u00a0$\\textsf{HB}$ are well-known cases of extensions of intuitionistic logic $\\textsf{Int}$ enriched with novel connectives. Wansing has suggested that G\u00f6del\u2019s provability interpretation of $\\textsf{Int}$ can be extended to these systems by pairing the category of formal proofs with a distinct category of formal refutations. In this paper, we extend the framework of Artemov\u2019s justification logic to provide explicit analyses of $\\textsf{N}$ and $\\textsf{HB}$ (and the dual-intuitionistic logic $\\textsf{DualInt}$) that respect a distinction between proofs and refutations. The application distinguishes the categories by reinterpreting the agents of multiple-agent justification logic as devices that operate exclusively on one or the other category. The analyses reveal that differences between $\\textsf{N}$ and $\\textsf{HB}$ can be reduced to competing interaction principles characterizing the coordination between proofs and refutations. We conclude by reappraising some of the unusual features of $\\textsf{HB}$ in light of the explicit analysis of $\\textsf{HB}$.<\/jats:p>","DOI":"10.1093\/logcom\/exaa047","type":"journal-article","created":{"date-parts":[[2020,10,2]],"date-time":"2020-10-02T11:09:56Z","timestamp":1601636996000},"page":"1505-1540","source":"Crossref","is-referenced-by-count":2,"title":["Explicit analyses of proof\/refutation interaction for constructible falsity and Heyting\u2013Brouwer logic"],"prefix":"10.1093","volume":"30","author":[{"given":"Thomas Macaulay","family":"Ferguson","sequence":"first","affiliation":[{"name":"Dun & Bradstreet, Austin, TX, 78729, USA; and Saul Kripke Center, City University of New York, New York. NY, 10016, USA"}]}],"member":"286","published-online":{"date-parts":[[2020,10,2]]},"reference":[{"key":"2020120307171367900_ref1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-09764-0_1","article-title":"On the complexity of two-agent justification logic","volume-title":"Computational Logic in Multi-Agent Systems","author":"Achilleos","year":"2014"},{"key":"2020120307171367900_ref2","article-title":"Operational modal logic","volume-title":"Technical Report MSI 95-29","author":"Artemov","year":"1995"},{"key":"2020120307171367900_ref3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-0-387-69245-6_1","article-title":"On two models of provability","volume-title":"Mathematical Problems from Applied Logics II","author":"Artemov","year":"2007"},{"key":"2020120307171367900_ref4","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":"2020120307171367900_ref5","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s11225-012-9387-x","article-title":"The ontology of justifications in the logical setting","volume":"100","author":"Artemov","year":"2012","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref6","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-540-73099-6_9","article-title":"A cut-free sequent calculus for bi-intuitionistic logic","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2007","author":"Buisman","year":"2007"},{"key":"2020120307171367900_ref7","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1093\/jigpal\/jzt027","article-title":"Strict paraconsistency of truth-degree preserving intuitionistic logic with dual negation","volume":"22","author":"Castiglioni","year":"2014","journal-title":"Logic Journal of the IGPL"},{"key":"2020120307171367900_ref8","volume-title":"A New Introduction to Modal Logic","author":"Cresswell","year":"1996"},{"key":"2020120307171367900_ref9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","article-title":"Subtractive logic","volume":"254","author":"Crolard","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"2020120307171367900_ref10","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","article-title":"A formulae-as-types interpretation of subtractive logic","volume":"14","author":"Crolard","year":"2004","journal-title":"Journal of Logic and Computation"},{"key":"2020120307171367900_ref11","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1305\/ndjfl\/1093891487","article-title":"On the theory of inconsistent formal systems","volume":"15","author":"da Costa","year":"1974","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2020120307171367900_ref12","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/s11225-013-9469-4","article-title":"Extensions of Priest-da Costa logic","volume":"102","author":"Ferguson","year":"2014","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1109\/ISMVL.2014.29","article-title":"\u0141ukasiewicz negation and many-valued extensions of constructive logics","volume-title":"Proc. 44th International Symposium on Multiple-Valued Logic (ISMVL 2014)","author":"Ferguson","year":"2014"},{"key":"2020120307171367900_ref14","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/978-3-319-72056-2_10","article-title":"A G\u00f6del-Artemov-style analysis of constructible falsity","volume-title":"Proc. International Symposium on Logical Foundations of Computer Science (LFCS 2018)","author":"Ferguson","year":"2018"},{"key":"2020120307171367900_ref15","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":"2020120307171367900_ref16","article-title":"Realization implemented","author":"Fitting","year":"2013"},{"key":"2020120307171367900_ref17","article-title":"Justification logics and realization","volume-title":"Technical Report TR-2014004","author":"Fitting","year":"2014"},{"key":"2020120307171367900_ref18","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1007\/s11225-017-9714-3","article-title":"Paraconsistent logic, evidence, and justification","volume":"105","author":"Fitting","year":"2017","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref19","first-page":"39","article-title":"Eine interpretation des intuitionistischen Aussagenkalk\u00fcls","volume":"4","author":"G\u00f6del","year":"1933","journal-title":"Ergebnisse eines Mathematischen Kolloquiums"},{"key":"2020120307171367900_ref20","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1093\/logcom\/exn067","article-title":"Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic","volume":"20","author":"Gor\u00e9","year":"2010","journal-title":"Journal of Logic and Computation"},{"key":"2020120307171367900_ref21","first-page":"205","article-title":"An embedding-based completeness proof for Nelson\u2019s paraconsistent logic","volume":"39","author":"Kamide","year":"2010","journal-title":"Bulletin of the Section of Logic"},{"key":"2020120307171367900_ref22","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-05206-9","volume-title":"Logics and Falsifications: A New Perspective on Constructivist Semantics","author":"Kapsner","year":"2014"},{"key":"2020120307171367900_ref23","doi-asserted-by":"crossref","first-page":"636","DOI":"10.1007\/s00224-009-9209-3","article-title":"Self-referential justification in epistemic logic","volume":"46","author":"Kuznets","year":"2010","journal-title":"Theory of Computing Systems"},{"key":"2020120307171367900_ref24","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1016\/1385-7258(72)90053-4","article-title":"Refutability and elementary number theory","volume":"75","author":"L\u00f3pez-Escobar","year":"1972","journal-title":"Indagationes Mathematicae"},{"key":"2020120307171367900_ref25","first-page":"80","article-title":"Modal interpretation of Heyting\u2013Brouwer logic","volume":"25","author":"\u0141ukowski","year":"1996","journal-title":"Bulletin of the Section of Logic"},{"key":"2020120307171367900_ref26","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":"Journal of Symbolic Logic"},{"key":"2020120307171367900_ref27","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/3-540-63045-7_27","article-title":"Models for the logic of proofs","volume-title":"Logical Foundations of Computer Science","author":"Mkrtychev","year":"1997"},{"key":"2020120307171367900_ref28","first-page":"185","article-title":"Paraconsistent logics obtained by J.-Y. B\u00e9ziau\u2019s method by means of some non-normal modal logics. I","volume":"37","author":"Mruczek-Nasieniewska","year":"2008","journal-title":"Bulletin of the Section of Logic"},{"key":"2020120307171367900_ref29","article-title":"Paraconsistent logics obtained by J.-Y. B\u00e9ziau\u2019s method by means of some non-normal modal logics. II","author":"Mruczek-Nasieniewska","year":"2011","journal-title":"Fourth International Conference on Non-Classical Logics, \u0141\u00f3d\u017a"},{"key":"2020120307171367900_ref30","doi-asserted-by":"crossref","first-page":"16","DOI":"10.2307\/2268973","article-title":"Constructible falsity","volume":"14","author":"Nelson","year":"1949","journal-title":"Journal of Symbolic Logic"},{"key":"2020120307171367900_ref31","first-page":"208","article-title":"Negation and separation of concepts in constructive systems","volume-title":"Constructivity in Mathematics","author":"Nelson","year":"1959"},{"key":"2020120307171367900_ref32","doi-asserted-by":"crossref","first-page":"231","DOI":"10.2307\/2274105","article-title":"Constructible falsity and inexact predicates","volume":"49","author":"Nelson","year":"1984","journal-title":"Journal of Symbolic Logic"},{"key":"2020120307171367900_ref33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-6867-6","volume-title":"Constructive Negations and Paraconsistency","author":"Odintsov","year":"2008"},{"key":"2020120307171367900_ref34","article-title":"A note on some explicit modal logics","volume-title":"Technical Report PP-2006-29","author":"Pacuit","year":"2006"},{"key":"2020120307171367900_ref35","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-642-02716-1_22","article-title":"Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)","author":"Pinto","year":"2009"},{"key":"2020120307171367900_ref36","first-page":"57","article-title":"Relating sequent calculi for bi-intuitionistic propositional logic","volume-title":"Proceedings of the Third International Workshop on Classical Logic and Computation","author":"Pinto","year":"2011"},{"key":"2020120307171367900_ref37","first-page":"165","article-title":"Dualising intuitionistic negation","volume":"13","author":"Priest","year":"2009","journal-title":"Principia"},{"key":"2020120307171367900_ref38","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future","author":"Prior","year":"1967"},{"key":"2020120307171367900_ref39","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF02120864","article-title":"A formalization of the propositional calculus of $\\textsf{H}$-$\\textsf{B}$ logic","volume":"33","author":"Rauszer","year":"1974","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref40","doi-asserted-by":"crossref","first-page":"219","DOI":"10.4064\/fm-83-3-219-249","article-title":"Semi-Boolean algebras and their application to intuitionistic logic with dual operations","volume":"83","author":"Rauszer","year":"1974","journal-title":"Fundamenta Mathematicae"},{"key":"2020120307171367900_ref41","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF02121115","article-title":"Applications of Kripke models to Heyting\u2013Brouwer logic","volume":"36","author":"Rauszer","year":"1977","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref42","first-page":"1","article-title":"An algebraic and Kripke-style approach to a certain extension of intuitionistic logic","volume":"167","author":"Rauszer","year":"1980","journal-title":"Dissertationes Mathematicae"},{"key":"2020120307171367900_ref43","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/11753728_32","article-title":"Evidence reconstruction of epistemic modal logic S5","volume-title":"Computer Science\u2014Theory and Applications (CSR 2006)","author":"Rubtsova","year":"2006"},{"key":"2020120307171367900_ref44","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1017\/S1755020316000022","article-title":"A modal translation for dual-intuitionistic logic","volume":"9","author":"Shramko","year":"2016","journal-title":"Review of Symbolic Logic"},{"key":"2020120307171367900_ref45","first-page":"513","article-title":"Paraconsistent justification logic: a starting point","volume-title":"Advances in Modal Logic","author":"Su","year":"2014"},{"key":"2020120307171367900_ref46","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1002\/malq.19690151602","article-title":"A semantical study of constructible falsity","volume":"15","author":"Thomason","year":"1969","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"2020120307171367900_ref47","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1007\/s11225-012-9417-8","article-title":"Natural deduction for dual-intuitionistic logic","volume":"100","author":"Tranchini","year":"2012","journal-title":"Studia Logica"},{"key":"2020120307171367900_ref48","first-page":"203","article-title":"Temporal logic","volume-title":"The Blackwell Guide to Philosophical Logic","author":"Venema","year":"2001"},{"key":"2020120307171367900_ref49","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-94-010-0387-2_2","article-title":"Sequent systems for modal logics","volume-title":"Handbook of Philosophical Logic","author":"Wansing","year":"2002"},{"key":"2020120307171367900_ref50","doi-asserted-by":"crossref","first-page":"341","DOI":"10.3166\/jancl.18.341-364","article-title":"Constructive negation, implication, and co-implication","volume":"18","author":"Wansing","year":"2008","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2020120307171367900_ref51","first-page":"483","article-title":"Proofs, disproofs, and their duals","volume-title":"Advances in Modal Logic","author":"Wansing","year":"2008"},{"key":"2020120307171367900_ref52","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1093\/logcom\/ext035","article-title":"Falsification, natural deduction and bi-intuitionistic logic","volume":"26","author":"Wansing","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"2020120307171367900_ref53","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1023\/A:1004218110879","article-title":"On logics with coimplication","volume":"27","author":"Wolter","year":"1998","journal-title":"Journal of Philosophical Logic"},{"key":"2020120307171367900_ref54","first-page":"369","article-title":"Multi-agent explicit knowledge","volume-title":"Computer Science\u2014Theory and Applications (CSR 2006)","author":"Sidon","year":"2006"},{"key":"2020120307171367900_ref55","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/s00224-007-9057-y","article-title":"Interacting explicit evidence systems","volume":"43","author":"Sidon","year":"2008","journal-title":"Theory of Computing Systems"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1505\/34673249\/exaa047.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1505\/34673249\/exaa047.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,3]],"date-time":"2020-12-03T12:20:05Z","timestamp":1606998005000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/8\/1505\/5916934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,2]]},"references-count":55,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2020,10,2]]},"published-print":{"date-parts":[[2020,12,10]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa047","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,12]]},"published":{"date-parts":[[2020,10,2]]}}}