# 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?

-
There is no "set theory in general", that's the point. But if you add certain axioms about large cardinals, then you can formalize category theory; even without them, you can formalize what is "almost as good" as category theory, namely small category theory (where the collection of all objects is a set, and the collection of all arrows between two objects is a set). –  Arturo Magidin Feb 25 '11 at 5:02
One can use NBG when dealing with categories. I'm sure one of out resident logicians will shortly come to the rescue.... –  Mariano Suárez-Alvarez Feb 25 '11 at 5:08
With some seriousness, I would give the following answer: "Yes -- set theory." –  Pete L. Clark Feb 25 '11 at 14:13
@Pete: Well, I would point out that, in fact, Goedel used set theory to formalize set theory (in the sense of constructing an "inner model" for set theory within set theory, V=L...) though that could be somewhat of a stretch, perhaps. –  Arturo Magidin Feb 26 '11 at 0:48
There is no technical reason that prevents someone from using ZFC as a metatheory for studying ZFC. The "metaverse axioms" of Joel Hamkins, Victoria Gitman, and their colleagues can be viewed as something of this sort, set theory studied within set theory. –  Carl Mummert Jun 14 '11 at 0:46

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...

-
+1 for choice sequences, which are an example of Brouwer at his most non-classical. –  Carl Mummert Jun 14 '11 at 0:54

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.

-