{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:37:14Z","timestamp":1740141434415,"version":"3.37.3"},"reference-count":12,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T00:00:00Z","timestamp":1595980800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["UIDB\/00013\/2020","UIDP\/00013\/2020","UID\/MAT\/04561\/2019","UID\/CEC\/00408\/2019"],"award-info":[{"award-number":["UIDB\/00013\/2020","UIDP\/00013\/2020","UID\/MAT\/04561\/2019","UID\/CEC\/00408\/2019"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9,24]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Given the recent interest in the fragment of system $\\mathbf{F}$ where universal instantiation is restricted to atomic formulas, a fragment nowadays named system ${\\mathbf{F}}_{\\textbf{at}}$, we study directly in system $\\mathbf{F}$ new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (i) they help achieving strict simulation of proof reduction by means of the Russell\u2013Prawitz embedding of $\\textbf{IPC}$ into system $\\mathbf{F}$, (ii) they are not stronger than a certain \u2018dinaturality\u2019 conversion known to generate a consistent equality of proofs, (iii) they provide the bridge between the Russell\u2013Prawitz embedding and another translation, due to the authors, of $\\textbf{IPC}$ directly into system ${\\mathbf{F}}_{\\textbf{at}}$ and (iv) they give means for explaining why the Russell\u2013Prawitz translation achieves strict simulation whereas the translation into ${\\mathbf{F}}_{\\textbf{at}}$ does not.<\/jats:p>","DOI":"10.1093\/jigpal\/jzaa025","type":"journal-article","created":{"date-parts":[[2020,6,25]],"date-time":"2020-06-25T11:25:14Z","timestamp":1593084314000},"page":"823-858","source":"Crossref","is-referenced-by-count":2,"title":["The Russell-Prawitz embedding and the atomization of universal instantiation"],"prefix":"10.1093","volume":"29","author":[{"given":"Jos\u00e9 Esp\u00edrito","family":"Santo","sequence":"first","affiliation":[{"name":"Centro de Matem\u00e1tica Universidade do Minho, 4710-057 Braga, Portugal"}]},{"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[{"name":"DCeT, Universidade Aberta, 1269-001 Lisboa, Portugal, CMAFcIO, Faculdade de Ci\u00eancias da Universidade de Lisboa, 1749-016 Lisboa, Portugal"}]}],"member":"286","published-online":{"date-parts":[[2020,7,29]]},"reference":[{"key":"2021091710535001600_ref1","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1017\/S0960129501003309","article-title":"The Russell\u2013Prawitz modality","volume":"11","author":"Aczel","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"2021091710535001600_ref2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","article-title":"Functorial polymorphism","volume":"70","author":"Bainbridge","year":"1990","journal-title":"Theoretical Computer Science"},{"key":"2021091710535001600_ref3","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/s11225-019-09858-1","article-title":"A refined interpretation of intuitionistic logic by means of atomic polymorphism","volume":"108","author":"Esp\u00edrito Santo","year":"2020","journal-title":"Studia Logica"},{"key":"2021091710535001600_ref4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10992-005-9001-z","article-title":"Comments on predicative logic","volume":"35","author":"Ferreira","year":"2006","journal-title":"Journal of Philosophical Logic"},{"key":"2021091710535001600_ref5","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s11225-009-9186-1","article-title":"Commuting conversions vs. the standard conversions of the \u2018good\u2019 connectives","volume":"92","author":"Ferreira","year":"2009","journal-title":"Studia Logica"},{"key":"2021091710535001600_ref6","first-page":"115","article-title":"Eta-conversions of $\\textbf{IPC}$ implemented in atomic $\\mathbf{F}$","volume":"25","author":"Ferreira","year":"2017","journal-title":"Logic Journal of IGPL"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"2021091710535001600_ref7"},{"key":"2021091710535001600_ref8","first-page":"267","article-title":"Dinatural terms in system F","volume-title":"In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science","author":"De Lataillade","year":"2009"},{"key":"2021091710535001600_ref9","article-title":"The naturality of natural deduction (II)","author":"Pistone","year":"2019","journal-title":"Some remarks on atomic polymorphism"},{"volume-title":"Natural Deduction","year":"1965","author":"Prawitz","key":"2021091710535001600_ref10"},{"key":"2021091710535001600_ref11","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s11225-017-9772-6","article-title":"The naturality of natural deduction","volume":"107","author":"Tranchini","year":"2019","journal-title":"Studia Logica"},{"volume-title":"Basic Proof Theory","year":"1996","author":"Troelstra","key":"2021091710535001600_ref12"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/5\/823\/40331094\/jzaa025.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/5\/823\/40331094\/jzaa025.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,17]],"date-time":"2021-09-17T11:09:39Z","timestamp":1631876979000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/29\/5\/823\/5877481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,29]]},"references-count":12,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2020,7,29]]},"published-print":{"date-parts":[[2021,9,24]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzaa025","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2021,10]]},"published":{"date-parts":[[2020,7,29]]}}}