The Finitistic Consistency of Heck’s Predicative Fregean System
Luı́s Cruz-Filipe, Fernando A.F. Ferreira · Notre Dame Journal of Formal Logic · 2015
Frege’s theory is inconsistent (Russell’s paradox). However, the predicative version of Frege’s system is consistent. This was proved by Richard Heck in 1996 using a model-theoretic argument. In this paper, we give a finitistic proof of this consistency result. As a consequence, Heck’s predicative theory is rather weak (as was suspected). We also prove the finitistic consistency of the extension of Heck’s theory to Δ11-comprehension and of Heck’s ramified predicative second-order system.