Post-Goedelian mathematics as an empirical inquiry

Once one absorbs the lessons of the Goedel incompleteness theorems, a formalist view of mathematics as just about logical relationships such as provability becomes unsupportable (for me the strongest indication of this is the independence of logical validity). Platonism thereby becomes more plausible (but even Platonism is not unproblematic, because mathematical Platonism tends towards plenitude, and given plenitude it is difficult to identify which natural numbers we mean).

But there is another way to see post-Goedelian mathematics, as an empirical and even experimental inquiry into the question of what can be proved by beings like us. While the abstract notion of provability is subject to Goedelian concerns, the notion of provability by beings like us does not seem to be, because it is not mathematically formalizable.

We can mathematically formalize a necessary condition for something to be proved by us which we can call “stepwise validity”: each non-axiomatic step follows from the preceding steps by such-and-such formal rules. To say that something can be proved by beings like us, then, would be to say that beings like us can produce (in speech or writing or some other relevantly similar medium) a stepwise valid sequence of steps that starts with the axioms and ends with the conclusion. This is a question about our causal powers of linguistic production, and hence can be seen as empirical.

Perhaps the surest way to settle the question of provability by beings like us is for us to actually produce the stepwise valid sequence of steps, and check its stepwise validity. But in practice mathematicians usually don’t: they skip obvious steps in the sequence. In doing so, they are producing a meta-argument that makes it plausible that beings like us could produce the stepwise valid sequence if they really wanted to.

This might seem to lead to a non-realist view of mathematics. Whether it does so depends, however, on our epistemology. If in fact provability by beings like us tracks metaphysical necessity—i.e., if B is provable by beings like us from A₁, ..., A_n, then it is not possible to have A₁, ..., A_n without B—then by means of provability by beings like us we discover metaphysical necessities.