MIRFoM
Metatheoretic and Intertheoretic Reductions in the Foundations of Mathematics
NCN OPUS grant · hosted by the University of Warsaw · September 2025 – 2029 · grant no. 2024/53/B/HS1/02173
About the project
Reductions are ubiquitous in studies of the foundations of mathematics. MIRFoM analyses two groups of such reductions: metatheoretic and intertheoretic reductions. Examples of the first kind are various formal explications of philosophical concepts (such as the explication of the concept of truth by means of axiomatic theories) and of standpoints, such as the so-called foundational equivalences between philosophical standpoints and formal theories. Examples of the second type consist of reductions between formal theories, such as interpretability, feasible interpretability, proof-theoretic reduction, or definability. The project analyses the epistemic significance of both types of reduction.
Metatheoretic reductions
Many natural formal theories in the foundations of mathematics seem to have a designated subject matter. Arithmetical theories like Peano Arithmetic (PA) are described as first-order theories of the arithmetic of natural numbers; subsystems of second-order arithmetic like arithmetical comprehension (ACA0) are designed to grasp real analysis; axiomatic theories of truth, such as compositional truth (CT) or the Kripke–Feferman theory of self-applicable truth (KF), formalise the notion of truth used in mathematical and informal reasoning; and set theories such as Zermelo–Fraenkel (ZF) grasp the concept of set. Metatheoretic reductions state that certain concepts or foundational standpoints are reducible to a formal theory. Without them there seems to be no connection between a formal theory and the (broadly construed) subject matter of an area of mathematics. The project aims to analyse this intuitive idea philosophically and to make it formally precise.
Intertheoretic reductions
Intertheoretic reductions are crucial tools in the proof-theoretic and model-theoretic analysis of formal theories, yet their epistemic status remains unclear: what philosophical consequences can we draw from the existence of a given reducibility relation between two theories? The project studies this question in the context of the conceptual content of a theory — for instance, in accepting ZFC as formalising the concept of set, one seems implicitly committed to concepts it does not explicitly formalise, such as that of a natural number. How strong must a reducibility relation between theories be to give rise to such conceptual commitments? The project proposes interpreting certain natural reducibility relations as a measure of the conceptual distance between theories.
Project outputs
- An Impossibility Result for Theories of Type-Free Determinateness. Analysis (forthcoming). A limitative theorem for type-free determinateness (admissibility) predicates. Preprint / published version
Further outputs will be added as the project progresses.
Get in touch
If you are interested in the themes of the project, or would like to discuss a possible collaboration — please get in touch.