The operational paradigm: its mathematical and philosophical frontiers

This proposal, consisting of two main parts, assesses the limits of mathematical knowledge inherent in and provided by an operational approach – an approach which plays a central role in Feferman’s explicit mathematics and operational set theory – from various mathematical and philosophical perspectives. The notion of predicativity goes back to Russell and Poincare and was formally made precise by Feferman and Schuette, who were also able to exactly characterize predicative mathematics. The first part of this proposal is about an extension of predicativity, which we call metapredicativity, in taking a more liberal approach to “building up set-theoretic universes from below”. We aim at a conceptually and technically convincing classification of those formal systems that are no longer predicative in the sense of Feferman-Schuette but whose proof-theoretic analysis can be carried through by purely predicative methods. Our solution should unravel this dichotomy by providing a foundationally convincing explanation. In addition, we aspire to determine the limit of metapredicativity. The second part is concerned with the design and analysis of strong operational systems and independence results making use of those. For this purpose, new extensions or generalizations of forcing and realizability techniques will be developed. The main products will be scientific results, documented in research articles. In addition, presentations of our results at international conferences, exchange visits, and the training of graduate students are envisaged. The long term impact of this project will provide convincing answers concerning the foundational relevance of an alternative approach to formalizing mathematics which, however, is closer to mathematical practice. If a far-reaching speculation is permitted: We may even gain new insights concerning Voevodsky’s univalent foundations by looking at them from an operational perspective.