Implication and analysis in classical Frege structures (Q1095139)

The authors construct a foundational system for mathematics on the Fregean concept of property, i.e. such that for any formula \(\Phi\) (x) there is a property \(\Psi\) such that \(\Phi\) (M) and ``M has property \(\Psi\) '' are interdeducible for every M. On this basis systems have been constructed by Fitch and Aczel. According to the authors the most reasonable foundation of classical mathematics based on Frege's concept of property is to define reals as Dedekind cuts and to use a hierarchy of implications. Such a system was proposed in 1975 by the second author, without a consistency proof, which is now supplied by exploiting Aczel's notion of Frege structure. In this paper the authors develop the proof theory and model theory of classical Frege structures, formalize the hierarchy of implications, prove the consistency of the system and outline the resulting analysis with Dedekind reals, which resembles to a large extent classical (elementary) analysis, and with Cauchy reals, which resembles recursive analysis.