{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,29]],"date-time":"2025-01-29T05:38:03Z","timestamp":1738129083629,"version":"3.33.0"},"reference-count":20,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T00:00:00Z","timestamp":1703808000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,2,27]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We present a uniform proof-theoretic proof of the G\u00f6del\u2013McKinsey\u2013Tarski embedding for a class of first-order intuitionistic theories. This is achieved by adapting to the case of modal logic the methods of proof analysis in order to convert axioms into rules of inference of a suitable sequent calculus. The soundness and the faithfulness of the embedding are proved by induction on the height of the derivations in the augmented calculi. Finally, we define an extension of the modal system for which the result holds with respect to geometric intuitionistic.<\/jats:p>","DOI":"10.1093\/jigpal\/jzad029","type":"journal-article","created":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T18:55:30Z","timestamp":1703962530000},"page":"149-172","source":"Crossref","is-referenced-by-count":0,"title":["Constructive theories through a modal lens"],"prefix":"10.1093","volume":"33","author":[{"given":"Matteo","family":"Tesi","sequence":"first","affiliation":[{"name":"Scuola Normale Superiore di Pisa, Classe di Lettere e Filosofia , 56126 Pisa, Italy and Technische Universit\u00e4t Wien, Institute of Logic and Computation, A-1040 Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2023,12,29]]},"reference":[{"key":"2025012810512750300_ref1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"Chagrov","year":"1997"},{"key":"2025012810512750300_ref2","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1002\/malq.19590051405","article-title":"Modal logics between S4 and S5","volume":"5","author":"Dummet","year":"1959","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"2025012810512750300_ref3","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s00153-011-0254-7","article-title":"Proof analysis in intermediate logic","volume":"51","author":"Dyckhoff","year":"2012","journal-title":"Archive for Mathematical Logic"},{"key":"2025012810512750300_ref4","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1093\/logcom\/ext036","article-title":"A cut-free sequent system for Grzegorczyk logic with an application to the G\u00f6del\u2013McKinsey\u2013Tarski embedding","volume":"26","author":"Dyckhoff","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"2025012810512750300_ref5","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0168-0072(86)90043-6","article-title":"Epistemic and intuitionistic formal systems","volume":"32","author":"Flagg","year":"1986","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025012810512750300_ref6","first-page":"39","article-title":"Eine interpretation der intuitionistischen aussagenkal\u00fcls","volume":"4","author":"G\u00f6del","year":"1933","journal-title":"Ergebnisse eines Mathematischen Kolloquiums"},{"key":"2025012810512750300_ref7","doi-asserted-by":"crossref","first-page":"192","DOI":"10.2307\/2274102","article-title":"Epistemic arithmetic is a conservative extension of intuitionistic arithmetic","volume":"49","author":"Goodman","year":"1984","journal-title":"Journal of Symbolic Logic"},{"key":"2025012810512750300_ref8","doi-asserted-by":"crossref","first-page":"282","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"Hughes","year":"1996"},{"key":"2025012810512750300_ref9","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":"2025012810512750300_ref10","article-title":"On Novikov hypothesis","volume-title":"Selected Papers in Proof Theory","author":"Mints","year":"1992"},{"key":"2025012810512750300_ref11","doi-asserted-by":"crossref","first-page":"418","DOI":"10.2307\/420956","article-title":"Cut elimination in the presence of axioms","volume":"4","author":"Negri","year":"1998","journal-title":"The Bulletin of Symbolic Logic"},{"key":"2025012810512750300_ref12","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s001530100124","article-title":"Contraction-free sequent calculi for geometric theories, with an application to Barr\u2019s theorem","volume":"42","author":"Negri","year":"2003","journal-title":"Archive for Mathematical Logic"},{"key":"2025012810512750300_ref13","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"Journal of Philosophical Logic"},{"volume-title":"The Mathematics of Metamathematics","year":"1963","author":"Rasiowa","key":"2025012810512750300_ref14"},{"key":"2025012810512750300_ref15","first-page":"1","article-title":"Topological representations of distributive lattices and Brouwerian logics","volume":"067","author":"Stone","year":"1937","journal-title":"Casopis pro Pestovan Matematiky a Fysiky"},{"key":"2025012810512750300_ref16","doi-asserted-by":"crossref","first-page":"1608","DOI":"10.1093\/logcom\/exab040","article-title":"Neighborhood semantics and labelled calculus for infinitary intuitionistic logic","volume":"31","author":"Tesi","year":"2020","journal-title":"Journal of Logic and Computation"},{"key":"2025012810512750300_ref17","doi-asserted-by":"crossref","first-page":"103285","DOI":"10.1016\/j.apal.2023.103285","article-title":"The G\u00f6del\u2013McKinsey\u2013Tarski embedding for infinitary intuitionistic logic and its extensions","volume":"174","author":"Tesi","year":"2023","journal-title":"Annals of Pure and Applied Logic"},{"volume-title":"Constructivism in Mathematics","year":"1998","author":"Troelstra","key":"2025012810512750300_ref18"},{"key":"2025012810512750300_ref19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2025012810512750300_ref20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logics","author":"Vigan\u00f2","year":"2000"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/1\/149\/54918625\/jzad029.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/1\/149\/54918625\/jzad029.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,28]],"date-time":"2025-01-28T10:51:50Z","timestamp":1738061510000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/33\/1\/149\/7502597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,29]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,2,27]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzad029","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2025,2]]},"published":{"date-parts":[[2023,12,29]]}}}