Ontological Purity for Formal Proofs

Robin Martinot

doi:10.1017/S1755020323000333

Ontological Purity for Formal Proofs

Robin Martinot

OFR - Theoretical Philosophy

Research output: Contribution to journal › Article › Academic › peer-review

Abstract

Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ 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 ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, 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.

Original language	English
Pages (from-to)	395-434
Number of pages	40
Journal	Review of Symbolic Logic
Volume	17
Issue number	2
Early online date	13 Nov 2023
DOIs	https://doi.org/10.1017/S1755020323000333
Publication status	Published - Jun 2024

Bibliographical note

Publisher Copyright:
© The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.

Funding

I gratefully acknowledge the support of the Netherlands Organisation for Scientific Research under grant 639.073.807.

Funders	Funder number
Netherlands Organisation for Scientific Research	639.073.807

Keywords

purity of proof
formalization
interpretations
structuralism
philosophy of proof theory

Access to Document

10.1017/S1755020323000333Licence: CC BY

ontological-purity-for-formal-proofsFinal published version, 426 KBLicence: CC BY

Cite this

@article{4a72dec9602e423cbcd9f716641fe568,

title = "Ontological Purity for Formal Proofs",

abstract = "Purity is known as an ideal of proof that restricts a proof to notions belonging to the {\textquoteleft}content{\textquoteright} 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 {\textquoteleft}fully ontologically pure{\textquoteright}. Formal proofs that refer to a surrogate ontological content of a theorem will be called {\textquoteleft}secondarily ontologically pure{\textquoteright}, 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.",

keywords = "purity of proof, formalization, interpretations, structuralism, philosophy of proof theory",

author = "Robin Martinot",

note = "Publisher Copyright: {\textcopyright} The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.",

year = "2024",

month = jun,

doi = "10.1017/S1755020323000333",

language = "English",

volume = "17",

pages = "395--434",

journal = "Review of Symbolic Logic",

issn = "1755-0203",

publisher = "Cambridge University Press",

number = "2",

}

TY - JOUR

T1 - Ontological Purity for Formal Proofs

AU - Martinot, Robin

N1 - Publisher Copyright: © The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.

PY - 2024/6

Y1 - 2024/6

N2 - Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ 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 ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, 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.

AB - Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ 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 ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, 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.

KW - purity of proof

KW - formalization

KW - interpretations

KW - structuralism

KW - philosophy of proof theory

UR - https://www.scopus.com/pages/publications/85178077755

U2 - 10.1017/S1755020323000333

DO - 10.1017/S1755020323000333

M3 - Article

SN - 1755-0203

VL - 17

SP - 395

EP - 434

JO - Review of Symbolic Logic

JF - Review of Symbolic Logic

IS - 2

ER -

Ontological Purity for Formal Proofs

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this