{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T12:17:28Z","timestamp":1771849048100,"version":"3.50.1"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2023,11,13]],"date-time":"2023-11-13T00:00:00Z","timestamp":1699833600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Purity is known as an ideal of proof that restricts a proof to notions belonging to the \u2018content\u2019 of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural deduction proofs of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called \u2018fully ontologically pure\u2019. Formal proofs that refer to a surrogate ontological content of a theorem will be called \u2018secondarily ontologically pure\u2019, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs.<\/jats:p>","DOI":"10.1017\/s1755020323000333","type":"journal-article","created":{"date-parts":[[2023,11,13]],"date-time":"2023-11-13T10:24:22Z","timestamp":1699871062000},"page":"395-434","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["ONTOLOGICAL PURITY FOR FORMAL PROOFS"],"prefix":"10.1017","volume":"17","author":[{"given":"ROBIN","family":"MARTINOT","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,11,13]]},"reference":[{"key":"S1755020323000333_r23","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1305\/ndjfl\/1193667707","article-title":"On interpretations of arithmetic and set theory","volume":"48","author":"Kaye","year":"2007","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S1755020323000333_r2","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-319-53385-8_16","volume-title":"Simplicity: Ideals of Practice in Mathematics and the Arts","author":"Arana","year":"2017"},{"key":"S1755020323000333_r10","doi-asserted-by":"crossref","first-page":"444","DOI":"10.4169\/amer.math.monthly.121.05.444","article-title":"A connection between Furstenberg\u2019s and Euclid\u2019s proofs of the infinitude of primes","volume":"121","author":"Carlson","year":"2014","journal-title":"The American Mathematical Monthly"},{"key":"S1755020323000333_r14","doi-asserted-by":"crossref","first-page":"286","DOI":"10.2307\/2307043","article-title":"On the infinitude of primes","volume":"62","author":"Furstenberg","year":"1955","journal-title":"American Mathematical Monthly"},{"key":"S1755020323000333_r18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"Hodges","year":"1993"},{"key":"S1755020323000333_r6","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1017\/S1755020312000263","article-title":"Formalization, primitive concepts, and purity","volume":"6","author":"Baldwin","year":"2013","journal-title":"Review of Symbolic Logic"},{"key":"S1755020323000333_r26","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1215\/00294527-2021-0003","article-title":"Impurity in contemporary mathematics","volume":"62","author":"Lehet","year":"2021","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S1755020323000333_r28","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1215\/00294527-2021-0004","article-title":"Induction, constructivity, and grounding","volume":"62","author":"McCarthy","year":"2021","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S1755020323000333_r33","doi-asserted-by":"crossref","first-page":"66","DOI":"10.4018\/978-1-61692-014-2.ch005","volume-title":"Thinking Machines and the Philosophy of Computer Science: Concepts and Principles","author":"Turner","year":"2010"},{"key":"S1755020323000333_r22","first-page":"125","volume-title":"The Logica Yearbook","author":"Kahle","year":"2017"},{"key":"S1755020323000333_r16","first-page":"198","volume-title":"Grundlagen der Geometrie","author":"Hallett","year":"2007"},{"key":"S1755020323000333_r24","first-page":"1","article-title":"Ground and explanation in mathematics","volume":"19","author":"Lange","year":"2019","journal-title":"Philosophers\u2019 Imprint"},{"key":"S1755020323000333_r29","doi-asserted-by":"crossref","first-page":"700","DOI":"10.1017\/S1755020321000538","article-title":"Szemer\u00e9di\u2019s theorem: An exploration of impurity, explanation, and content","volume":"16","author":"Ryan","year":"2021","journal-title":"Review of Symbolic Logic"},{"key":"S1755020323000333_r9","volume-title":"Handbook of Proof Theory","author":"Buss","year":"1998"},{"key":"S1755020323000333_r15","doi-asserted-by":"crossref","first-page":"265","DOI":"10.2178\/jsl\/1231082312","article-title":"Arithmetic on semigroups","volume":"74","author":"Ganea","year":"2009","journal-title":"Journal of Symbolic Logic"},{"key":"S1755020323000333_r4","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1017\/S1755020312000020","article-title":"On the relationship between plane and solid geometry","volume":"5","author":"Arana","year":"2012","journal-title":"Review of Symbolic Logic"},{"key":"S1755020323000333_r17","doi-asserted-by":"crossref","first-page":"20180040","DOI":"10.1098\/rsta.2018.0040","article-title":"Discussing Hilbert\u2019s 24th problem","volume":"377","author":"Hipolito","year":"2019","journal-title":"Philosophical Transactions of the Royal Society A"},{"key":"S1755020323000333_r27","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-030-15655-8_13","volume-title":"Reflections on the Foundations of Mathematics","author":"Maddy","year":"2019"},{"key":"S1755020323000333_r21","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0049-237X(09)70552-X","volume-title":"Logic Colloquium \u201885: Proceedings of the Colloquium held in Orsay, France, July 1985","volume":"122","author":"Isaacson","year":"1987"},{"key":"S1755020323000333_r25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005257423415","article-title":"Quantification and ontology","volume":"124","author":"Lavine","year":"2000","journal-title":"Synthese"},{"key":"S1755020323000333_r11","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1093\/philmat\/nkl009","article-title":"Why do mathematicians re-prove theorems?","volume":"14","author":"Dawson","year":"2006","journal-title":"Philosophia Mathematica"},{"key":"S1755020323000333_r12","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1093\/acprof:oso\/9780199296453.003.0008","volume-title":"The Philosophy of Mathematical Practice","author":"Detlefsen","year":"2008"},{"key":"S1755020323000333_r13","first-page":"1","article-title":"When bi-interpretability implies synonymy","volume":"320","author":"Friedman","year":"2014","journal-title":"Logic Group Preprint Series"},{"key":"S1755020323000333_r3","first-page":"1","article-title":"Purity of methods","volume":"11","author":"Arana","year":"2011","journal-title":"Philosophers\u2019 Imprint"},{"key":"S1755020323000333_r20","unstructured":"[20] Incurvati, L. , & Nicolai, C. (2020). On logical and scientific strength. Unpublished manuscript. Available from: https:\/\/philarchive.org\/archive\/INCOLA."},{"key":"S1755020323000333_r31","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/philmat\/nkm042","article-title":"Identity, indiscernibility, and ante rem structuralism: The tale of I and -I","volume":"16","author":"Shapiro","year":"2008","journal-title":"Philosophia Mathematica"},{"key":"S1755020323000333_r7","unstructured":"[7] Bolzano, Bernard (1817). Die drey Probleme der Rectifikation, der Complanation und der Cubierung, ohne Betrachtung des unendlich Kleinen, ohne die Annahme des Archimedes und ohne irgend eine nicht streng erweisliche Voraussetzung gel\u00f6st; zugleich als Probe einer g\u00e4nzlichen Umgestaltung der Raumwissenschaft allen Mathematikern zur Pr\u00fcfung vorgelegt. Leipzig: Gotthelf Kummer."},{"key":"S1755020323000333_r32","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/BF00499820","article-title":"Structural representation and surrogative reasoning","volume":"87","author":"Swoyer","year":"1991","journal-title":"Synthese"},{"key":"S1755020323000333_r5","doi-asserted-by":"crossref","first-page":"7377","DOI":"10.1007\/s11229-019-02524-y","article-title":"Reliability of mathematical inference","volume":"198","author":"Avigad","year":"2021","journal-title":"Synthese"},{"key":"S1755020323000333_r8","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780199278534.001.0001","volume-title":"Truth, Thought, Reason: Essays on Frege","volume":"1","author":"Burge","year":"2005"},{"key":"S1755020323000333_r19","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/978-3-319-53385-8_12","volume-title":"Simplicity: Ideals of Practice in Mathematics and the Arts","author":"Iemhoff","year":"2017"},{"key":"S1755020323000333_r1","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1093\/philmat\/nkn015","article-title":"On formally measuring and eliminating extraneous notions in proofs","volume":"17","author":"Arana","year":"2009","journal-title":"Philosophia Mathematica"},{"key":"S1755020323000333_r34","volume-title":"An Overview of Interpretability Logic","volume":"174","author":"Visser","year":"1997"},{"key":"S1755020323000333_r30","volume-title":"Philosophy of Mathematics: Structure and Ontology","author":"Shapiro","year":"1997"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020323000333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T13:20:25Z","timestamp":1716816025000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020323000333\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,13]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["S1755020323000333"],"URL":"https:\/\/doi.org\/10.1017\/s1755020323000333","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,13]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}