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?
-
0Which set theory? One cannot really formalize Category Theory in ZFC, because one cannot talk about, e.g., the category of all groups in ZFC. – 2011-02-25
-
0Set theory in general? If category theory cannot be formalised in ZFC, is there are another system in which it can be formalised? – 2011-02-25
-
5There 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). – 2011-02-25
-
5One can use NBG when dealing with categories. I'm sure one of out resident logicians will shortly come to the rescue.... – 2011-02-25
-
6With some seriousness, I would give the following answer: "Yes -- set theory." – 2011-02-25
-
1@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. – 2011-02-26
-
0Isn't one of the ZFC axioms actually an axiom schema that generates an axiom when given a set? You can't universally quantify that "axiom" since you'd have to start with "for any set S in the set of all sets", which doesn't exist, no? – 2011-03-13
-
1Most set-theorists regard the treatment of universes in category theory as rather clumsy in comparison with the far richer and subtle theory of large cardinals in set theory, of which it is a very small part. And to my knowledge, all the answers to foundational questions about the strength of the various universe axioms in category theory have come from set theory. – 2011-06-13
-
2There 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. – 2011-06-14
-
0Thanks, Carl! (Here is the paper to which I think you refer: http://arxiv.org/abs/1104.4450) – 2011-06-14
-
0@Carl: in my old comment above I didn't mean to suggest that it was somehow forbidden or strictly impossible to study set theory using set theory. That would be a strangely counterfactual statement, since after all contemporary set theorists do this. My point was rather that this is an incredibly complicated and delicate game: we do not know that the ZFC axioms are consistent, they are certainly incomplete, and so forth. So it seems that set theory has not been (completely) formalized, at least not yet. – 2011-06-14
2 Answers
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+1 for choice sequences, which are an example of Brouwer at his most non-classical. – 2011-06-14
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.