TL;DR
This paper explores Mostowski's 1950 results showing GB's conservativity over ZF and its role in providing a truth-definition for ZF-formulae, connecting Tarski-style truth theories with second order arithmetic.
Contribution
It offers an expository account of Mostowski's construction and demonstrates how it links Tarski-style truth theories over PA with subsystems of second order arithmetic.
Findings
GB is conservative over ZF.
GB provides a truth-definition for ZF-formulae.
The construction bridges Tarski-style truth theories with second order arithmetic.
Abstract
In 1950, Novak and Mostowski showed that GB (G\"odel-Bernays theory of classes) is conservative over ZF, and therefore by G\"odel's second incompleteness theorem the consistency of ZF is unprovable in GB. In the same year Mostowski unveiled a contrasting result: GB provides a truth-definition for ZF-formulae. Here we first give an expository account of Mostowski's construction and surrounding results, and then we show that the construction bridges the domain of Tarski-style truth theories over PA with certain subsystems of second order arithmetic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsStructural Engineering and Vibration Analysis · Transportation Safety and Impact Analysis · Geotechnical Engineering and Underground Structures