Review of Symbolic Logic:1-44 (forthcoming)

Patrick Walsh
Carnegie Mellon University
Wilfried Sieg
Carnegie Mellon University
Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at (see link below).
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1017/s175502031900056x
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,287
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
Cantor Theorem and Friends, in Logical Form.Silvio Valentini - 2013 - Annals of Pure and Applied Logic 164 (4):502-508.
Grim, Omniscience, and Cantor’s Theorem.Martin Lembke - 2012 - Forum Philosophicum: International Journal for Philosophy 17 (2):211-223.
Boolean Sentence Algebras: Isomorphism Constructions.William P. Hanf & Dale Myers - 1983 - Journal of Symbolic Logic 48 (2):329-338.
Cantor’s Proof in the Full Definable Universe.Laureano Luna & William Taylor - 2010 - Australasian Journal of Logic 9:10-25.
A Negation-Free Proof of Cantor's Theorem.N. Raja - 2005 - Notre Dame Journal of Formal Logic 46 (2):231-233.
Size and Function.Bruno Whittle - 2018 - Erkenntnis 83 (4):853-873.


Added to PP index

Total views
9 ( #848,637 of 2,325,533 )

Recent downloads (6 months)
2 ( #449,490 of 2,325,533 )

How can I increase my downloads?


My notes