Are there any areas of mathematics that are known to be impossible to formalise in terms of set theory?

Are there any areas of mathematics that are known to be impossible to formalise in terms of set theory?

Solution 1:

By set theory, I assume you mean ZFC rather than the many alternatives. As discussed in the comments, some mathematical objects are simply too large to be sets. However, there are many ways to work around such problematic objects. There are other types of problematic cases that are much harder to work around. For example, mathematical objects that defy formalization in set theory because they are inherently vague. I recall a great talk by Andreas Blass where he discussed a few such examples.

One example is the idea of a feasible number. The set $F$ of feasible numbers satisfies:

• $0 \in F$

• If $n \in F$ then $n + 1 \in F$

• $10^{9565} \notin F$

Clearly, the set $F$ does not exist in any classical set theory like ZFC. However, the concept of feasible number is definitely a real mathematical concept. Indeed, I recall a famous number theorist telling me "$\log\log n$ is never greater than $10$" — which is indeed true for all feasible $n$. Also, many have worked very hard to give a rigorous foundation for feasible numbers (e.g., Rohit Parikh, Vladimir Sazonov).

Another example is Brouwer's notion of a free choice sequence. These behave much like using a fair coin to generate an infinite sequence of 0's (tails) and 1's (heads): at any point you only know a finite initial segment of the sequence, and you don't know anything about the remaining elements of the sequence. The universe of sets is static and thus everything is known (at least in the above sense). For that reason, it is probably impossible to formalize free choice sequences in ZFC. Nevertheless, free choice sequences make sense and they have been used to prove theorems in intuitionistic arithmetic.

That said, some alternative set theories have been proposed to handle such difficult objects. For example, Petr Hájek suggested using the theory of semisets to formalize the notion of feasible numbers. So, perhaps, everything is formalizable in some set theory...

Solution 2:

The notion of constructive proof in mathematics, as understood by constructivists themselves, is an inherently informal notion. There are certainly many formalized analogues of constructive mathematics, which are worth studying. But constructivists reject the notion that any of these captures the notion of constructive proof, and they often make the stronger claim that constructive proof cannot be formalized.