{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:18Z","timestamp":1759637718457},"reference-count":34,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2022,11,8]],"date-time":"2022-11-08T00:00:00Z","timestamp":1667865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,12,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>G\u00f6del\u2019s Dialectica interpretation was designed to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic and double negation. In recent years, proof theoretic transformations (the so-called proof interpretations) based on G\u00f6del\u2019s Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on \u2018G\u00f6del fibrations\u2019, we present a (hyper)doctrine characterization of the Dialectica, which corresponds exactly to the logical description of the interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle and the Independence of Premise principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. We make sure that this tight correspondence extends to the use of the principles above, instead of the weaker rules we had proved earlier on. This tight correspondence should come handy not only when discussing the traditional applications of the Dialectica but also when dealing with newer uses in modelling games or concurrency theory.<\/jats:p>","DOI":"10.1093\/logcom\/exac079","type":"journal-article","created":{"date-parts":[[2022,10,4]],"date-time":"2022-10-04T12:44:39Z","timestamp":1664887479000},"page":"1855-1875","source":"Crossref","is-referenced-by-count":3,"title":["Dialectica logical principles: not only rules"],"prefix":"10.1093","volume":"32","author":[{"given":"Davide","family":"Trotta","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Pisa, Piano Secondo , Largo Bruno Pontecorvo, 3, 56127 Pisa PI, Italy"}]},{"given":"Matteo","family":"Spadetto","sequence":"additional","affiliation":[{"name":"School of Mathematics, University of Leeds, Woodhouse Lane , Leeds LS2 9JT, United Kingdom"}]},{"given":"Valeria","family":"de Paiva","sequence":"additional","affiliation":[{"name":"Topos Institute, 2140 Shattuck Ave, Suite 610 Berkeley , CA 94704, USA"}]}],"member":"286","published-online":{"date-parts":[[2022,11,8]]},"reference":[{"key":"2022121408225391300_ref1","article-title":"On natural deduction for Herbrand constructive logics II: Curry\u2013Howard correspondence for Markov\u2019s Principle in first-order logic and arithmetic","author":"Aschieri","year":"2016"},{"key":"2022121408225391300_ref2","first-page":"02","article-title":"G\u00f6del\u2019s functional (Dialectica) interpretation","volume":"137","author":"Avigad","year":"1970","journal-title":"Handbook of Proof Theory"},{"key":"2022121408225391300_ref3","first-page":"47","article-title":"The Dialectica categories","volume":"92","author":"de Paiva","year":"1989","journal-title":"Categories in Computer Science and Logic"},{"key":"2022121408225391300_ref4","article-title":"Categories of partial equivalence relations as localizations","author":"Frey","year":"2020"},{"key":"2022121408225391300_ref5","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","article-title":"\u00dcber eine bisher noch nicht ben\u00fctzte erweiterung des finiten standpunktes","volume":"12","author":"G\u00f6del","year":"1958","journal-title":"Dialectica"},{"key":"2022121408225391300_ref6","volume-title":"Kurt G\u00f6del: Collected Works: Volume II: Publications 1938\u20131974","author":"G\u00f6del","year":"1986"},{"key":"2022121408225391300_ref7","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1109\/LICS.2010.49","article-title":"An intuitionistic logic that proves Markov\u2019s principle","volume-title":"2010 25th Annual IEEE Symposium on Logic in Computer Science","author":"Herbelin","year":"2010"},{"key":"2022121408225391300_ref8","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1090\/crmp\/053\/05","article-title":"The Dialectica monad and its cousins","volume":"53","author":"Hofstra","year":"2011","journal-title":"Models, Logics, and Higher Dimensional Categories: A tribute to the Work of Mih\u00e1ly Makkai"},{"key":"2022121408225391300_ref9","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","article-title":"Tripos theory","volume":"88","author":"Hyland","year":"1980","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"2022121408225391300_ref10","article-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"2022121408225391300_ref11","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","article-title":"Adjointness in foundations","volume":"23","author":"Lawvere","year":"1969","journal-title":"Dialectica"},{"key":"2022121408225391300_ref12","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/BFb0080769","article-title":"Diagonal arguments and cartesian closed categories","volume-title":"Category Theory, Homology Theory and Their Applications","author":"Lawvere","year":"1969"},{"key":"2022121408225391300_ref13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/pspum\/017\/0257175","article-title":"Equality in hyperdoctrines and comprehension schema as an adjoint functor","volume-title":"New York Symposium on Application of Categorical Algebra","author":"Lawvere","year":"1970"},{"key":"2022121408225391300_ref14","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1017\/S0960129505004962","article-title":"Modular correspondence between dependent type theories and categories including pretopoi and topoi","volume":"15","author":"Maietti","year":"2005","journal-title":"Mathematical Structures in Computer Science"},{"key":"2022121408225391300_ref15","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1515\/tmj-2017-0106","article-title":"Triposes, exact completions, and Hilbert\u2019s $\\varepsilon $-operator","volume":"10","author":"Maietti","year":"2017","journal-title":"Tbilisi Mathematical Journal"},{"key":"2022121408225391300_ref16","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/s11787-013-0080-2","article-title":"Quotient completion for the foundation of constructive mathematics","volume":"7","author":"Maietti","year":"2013","journal-title":"Logica Universalis"},{"key":"2022121408225391300_ref17","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s10485-013-9360-5","article-title":"Unifying exact completions","volume":"23","author":"Maietti","year":"2013","journal-title":"Applied Categorical Structures"},{"key":"2022121408225391300_ref18","first-page":"229","volume-title":"Relating Quotient Completions via Categorical Logic","author":"Maietti","year":"2016"},{"key":"2022121408225391300_ref19","article-title":"Computational interpretations of Markov\u2019s principle","author":"Manighetti","year":"2016"},{"key":"2022121408225391300_ref20","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1145\/3209108.3209207","article-title":"Dialectica models of type theory","volume-title":"33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"Moss","year":"2018"},{"key":"2022121408225391300_ref21","article-title":"The independence of premise rule in intuitionistic set theories","author":"Nemoto","year":"2019"},{"key":"2022121408225391300_ref22","doi-asserted-by":"crossref","DOI":"10.1145\/2603088.2603094","article-title":"A functional functional interpretation","volume-title":"CSL-LICS 2014 Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"P\u00e9drot","year":"2014"},{"key":"2022121408225391300_ref23","first-page":"39","article-title":"Categorical logic","volume-title":"Handbook of Logic in Computer Science","author":"Pitts","year":"1995"},{"key":"2022121408225391300_ref24","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1017\/S096012950200364X","article-title":"Tripos theory in retrospect","volume":"12","author":"Pitts","year":"2002","journal-title":"Mathematical Structures in Computer Science"},{"key":"2022121408225391300_ref25","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1002\/malq.19940400203","article-title":"Cut-elimination theorem for the logic of constant domains","volume":"40","author":"Shimura","year":"1994","journal-title":"Mathematical Logic Quarterly"},{"key":"2022121408225391300_ref26","article-title":"Constructivism in Mathematics: An Introduction","volume-title":"Constructivism in Mathematics, Vol 1","author":"Troelstra","year":"1988"},{"key":"2022121408225391300_ref27","first-page":"1576","article-title":"The existential completion","volume":"35","author":"Trotta","year":"2020","journal-title":"Theory and Applications of Categories"},{"key":"2022121408225391300_ref28","article-title":"Generalized existential completions and their regular and exact completions","author":"Maietti","year":"2021"},{"key":"2022121408225391300_ref29","article-title":"Quantifier completions, choice principles and applications","author":"Trotta","year":"2020"},{"key":"2022121408225391300_ref30","article-title":"The G\u00f6del fibration (long version)","author":"Trotta","year":"2020"},{"key":"2022121408225391300_ref31","first-page":"87:1","article-title":"The G\u00f6del Fibration","volume-title":"46th International Symposium on Mathematical Foundations of Computer Science (2021)","author":"Trotta","year":"2021"},{"key":"2022121408225391300_ref32","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/978-3-030-93100-1_22","article-title":"Dialectica logical principles","volume-title":"Logical Foundations of Computer Science","author":"Trotta","year":"2022"},{"key":"2022121408225391300_ref33","volume-title":"Realizability: An Introduction to Its Categorical Side","author":"van Oosten","year":"2008"},{"key":"2022121408225391300_ref34","article-title":"Making concurrency functional","author":"Winskel","year":"2022"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/8\/1855\/47846344\/exac079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/8\/1855\/47846344\/exac079.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,14]],"date-time":"2022-12-14T11:43:20Z","timestamp":1671018200000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/32\/8\/1855\/6795172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,8]]},"references-count":34,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2022,11,8]]},"published-print":{"date-parts":[[2022,12,9]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exac079","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,12]]},"published":{"date-parts":[[2022,11,8]]}}}