Real reverse mathematics

Question

Standard mathematical developments, be they set theoretic, type theoretic, synthetic, etc. all follow the same basic pattern:

Lay out a language, assume some stuff in this language, then prove that other things are true relative to what we assumed and some agreed-upon logical system.

Modern developments in set theory (and other fields) have begun exploring what happens as we vary the stuff we assume, induced to do so by statements $\varphi$ that are independent of whatever our current assumptions are but still of interest to us.

More generally, it seems that each mathematician $M$ has some collection of statements $\Phi_M$ which they hold to be 'true' independent of which axiomatic system they're working in, and the validity of a given foundation $\mathfrak{F}$ to mathematician $M$ is measured to some extent by the degree to which $$\mathfrak{F}\vdash\Phi_M,$$ that is the extent to which the given foundation can prove that the things we hold to be true are actually true, and how easily the given foundation can establish these 'facts'. Things begin to get hairy when we have statements $\varphi,\varphi'\in\Phi_M$ which are independent of some standard agreed upon foundation $\mathfrak{F}_{reasonable}$, and are mutually exclusive in the sense that $$\mathfrak{F}_{reasonable}+\varphi\vdash\neg\varphi' \hspace{5mm} \text{and} \hspace{5mm} \mathfrak{F}_{reasonable}+\varphi'\vdash\neg\varphi,$$ for example taking $\mathfrak{F}_{reasonable}=ZF$, with $\varphi={\sf axiom\ of\ choice}$ and $\varphi'={\sf axiom\ of\ determinacy}.$

I am curious if there has ever been an attempt to codify this pattern of interaction between mathematician and foundation, taking $\Phi_M$ to be the 'primitive thing' and then exploring which foundations satisfy the above relationship. This obviously runs into some issues at primitive levels, i.e. where are we carrying out this investigation if what we are investigating are the places where we usually investigate stuff, and I have some ideas for how to address this issue but am curious how others might have remedied it. Further, we run into the question of why $\Phi_M$ itself should not always just form the foundation that mathematician $M$ uses. Any pointers or relevant discussion are appreciated.

Answer 1

Converted from comments:

You seem to be taking $\Phi_M$ as given and using it to guide your choice of a foundation. But my choice of a foundation can affect the contents of $\Phi_M$.

Consider a statement $X$ that I hold to be true about the sort of sets that are described by $ZFC$ but not about the sort of sets that are described by $NF$. Then $X$ is a member of $\Phi_M$ if I choose $ZFC$ as a foundation, but not if I choose $NF$.

So maybe you're looking for a fixed point of the process $\Phi_M\rightarrow$ foundation $\rightarrow \Phi_M$ ?

This problem goes away if $\Phi_M$ consists of statements about mathematical objects for which our intuitions precede any knowledge of foundations, such as the natural numbers. I see that you addressed this in your comment exchange with James Hanson, where you referred to statements about the real and complex numbers. But I'm not sure that works, because my intuitions about the real numbers (unlike my intuitions about the natural numbers) are, I suspect, partly dependent on my intuitions about set theory, so not as foundation-independent as they need to be.

Answer 2

Regarding your question of why we don't just take $\Phi_M$ to be the foundation, there's a well-known "inexhaustibility" difficulty coming from Gödel's theorem. I quote from the first page of Torkel Franzén's book Inexhaustibility: A Non-Exhaustive Treatment, who in turn quotes Gödel himself.

It is this theorem [the second incompleteness theorem] which makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct, and moreover I believe that they contain all of mathematics. If somebody makes such a statement he contradicts himself. For if he perceives the axioms under consideration to be correct, he also perceives (with the same certainty) that they are consistent. Hence he has a mathematical insight not derivable from his axioms.

The above observation has been invoked by some people to argue that humans are superior to computers; such arguments are dubious at best, but the underlying insight articulated by Gödel is correct. Franzén's book is an enlightening and entertaining account of what happens if you pursue this insight in a sustained way, and try repeatedly (and unsuccessfully) to wriggle out of it.

Here's a real-life example. On the Foundations of Mathematics mailing list, Arnon Avron recently posted something about a philosophy of mathematics called "predicativism," which he is championing as a secure foundation for mathematics. A frequently-made claim is that predicativism is captured by the Feferman–Schütte ordinal, but Avron, agreeing with Nik Weaver, rejects this characterization. Among the objections put forward by Weaver and Avron to the Feferman–Schütte analysis is a version of inexhaustibility: any account of what a hypothetical rational person (in this case, a predicativist) accepts cannot plausibly draw a sharp line at a particular ordinal, because any persuasive argument that everything up to that ordinal is sound is also going to be a persuasive argument that the ordinal itself is sound.

Answer 3

Here an interesting case study concerns the case $M=$ Leibniz. We have undertaken some detailed studies of primary documents recently, resulting in publications in the British Journal for the History of Mathematics and elsewhere, and I can report on a few conclusions that are particularly relevant to this question.

1. $\Phi_{\text{Leibniz}}$ assumes the validity of the part-whole principle as applied to infinite domains. This implies that what Leibniz refers to as "infinite wholes" is a contradictory concept and therefore useless in mathematics, according to Leibniz.

2. In view of the above, the Peano Arithmetic would be a better starting point for a Leibnizian $\mathfrak F$ than ZF.

3. Working within ordinary numbers, Leibniz assumes the existence of a primitive predicate he calls "assignable". Leibniz uses the term infinitum terminatum for an inassignable number bigger than each assignable number. The term sounds somewhat paradoxical to a modern ear in English translation: "bounded infinity" (this does not of course refer to an ordinal or cardinal but rather a member of a ring such as $\mathbb Z$ whose properties can be formalized in PA). The inverse of such a number gives an infinitesimal.

4. Karel Hrbacek and I have developed an effective foundation for real analysis with infinitesimals in a foundational system we called SPOT (an acronym for its axioms). This is effective in the sense of being conservative over ZF (without choice). Since SPOT incorporates ZF, it is not fully faithful to a Leibnizian foundation (see items 1 and 2).

5. A better foundation for $\Phi_{\text{Leibniz}}$ would perhaps be some jazzed-up version of Peano Arithmetic incorporating the assignable primitive.