Are there areas of mathematics (current or future) that cannot be formalized in set theory?

I often read that ZFC can formalize "most" of everyday mathematics, but I could never find an example which it cannot. The closest I got is differential geometry (DF), where some article mentions that the translation from concepts of DF into set theory would render it almost "meaningless", in the sense that any intuitions one could have would be lost in the translation. So, if I didn't misunderstand, at least in theory, the translation could be done, so that a future AI machine could prove theorems of differential geometry using set theory. On the other hand, the Stanford Encyclopedia of Philosophy states that "all of mathematics can be reduced to a formal system of set theory"(http://plato.stanford.edu/entries/set-theory/).

So, the questions are: 1) Is there any current area of mathematics that could be not formalized within set theory? If so, which ones? and 2) Is there any reason to think that every math of the future will be always formalizable in set theory? any references to read on the subject are welcomed! clarification: by set theory I am not restricting to ZFC, but to any flavor of it, including all additional axioms you want (about large cardinals or any kind)

-
Grothendieck topologies, which are used in algebraic geometry, require the existence of "large cardinals," an extension to ZFC. –  Thomas Andrews Feb 26 '13 at 14:37
thanks, I will edit the question, I meant set theory of any flavor –  julian fernandez Feb 26 '13 at 14:38
Sorry, that should be cohomologies, not topologies. But the dependency is still there. –  Thomas Andrews Feb 26 '13 at 14:59
IMHO, the translation of every (possible) area of mathematics into "formal set theory" (in which one is only allowed to talk about the $\in$ relationship and equality) renders it meaningless. This includes contemporary set theory itself! –  Arthur Fischer Feb 26 '13 at 16:13
@ThomasAndrews Both claims are false. It is perfectly possible to develop topos-theoretic cohomology within NBG, and with some work and care you can even do it directly in ZFC. Now, if you want to apply it to sites that algebraic geometers care about, however... –  Zhen Lin Feb 26 '13 at 17:12

First let me point out that set theory is a foundation to mathematics as much as electric current is the actual way a computer "thinks". You don't even have to go that far, you can go to the machine code itself.

Have you ever looked at a disassembled code? It takes a piece of code that was compiled from, perhaps, a high level language (such as C++, Visual Basic, C#, and so on), and it shows you what are the operations sent to the computer. It is very un-enlightening about the purpose of the original code, unless the original code itself was in assembly. But it still works.

In a similar way translating everything into the language of $\{\in\}$ and sets ends up in a very strange result, often allowing for insane type errors (e.g. $\{\langle 0,1\rangle\}\subseteq 4$). But the point of foundational set theory is not to have a sensible translation, but to have some sort of a consistent CPU where mathematics can be executed. In this aspect set theory allows us to turn everything into first-order logic theories, where we can apply completeness, incompleteness and deduction theorems on them.

Classic mathematics such as calculus, basic linear algebra, measure theory, classic functional analysis, those things can be easily modeled in ZFC. Truth to be told, ZFC is a lot stronger than needed, and there are people nowadays working on using arithmetics (usually second-order arithmetics, or weakening of it) as the use of foundational theory.

However the more mathematics progressed into abstractions and infinite there were points that were not within the reach of "vanilla ZFC". For example classes, classes of classes, a lot of category theory, etc.

While it is possible to switch from ZFC to NBG, which is a conservative extension which allows classes, one turns into a two-sorted theory which is often slightly less convenient, but it to can only take you so far and not always enough. So Grothendieck suggested universes, which was a concept later used for the Tarski-Grothendieck set theory which itself is an extension of ZFC. But large cardinals allow us to correct this situation as well. Large cardinals allow us to have frameworks much stronger than universes. In fact the TG set theory is equivalent to some large cardinal additions to ZFC.

Speaking of large cardinals, we can go further, it has been suggested that there is a deep connection between some concepts in model categories and homotopy theory and large cardinals. I am not familiar with the details, but I had a couple of short chats with a few people who do, and it seems that in order to formalize some general notion of model category apparently you end up using a lot more than inaccessible cardinals (the words Vopenka principle come to mind). But that too is within the reach of ZFC+suitable large cardinal axioms.

What cannot be formalized in set theory? Well. Nobody knows the future, I can only assert with certainty that at some point we die. Currently I believe that the way we think about mathematics is such that essentially everything can be turn into set theory. In particular ZFC+axioms which have not yet been proven inconsistent with ZFC.

But let us turn our heads, for a moment, to the other side of set theory. Algebraic set theory. The idea is not to put emphasis on elements and membership structure, but rather on functions between our sets. Such set theories like ETCS have been proposed as foundation for a lot of the mathematics in place of the classical ZFC foundations. There has been a lot of discussions over the topic a month ago after a paper called "Rethinking Set Theory" by Tom Leister was posted online. Taking part in those discussions I have learned two things that I have known before:

1. Whenever you take "concrete mathematics" (e.g. analysis, measure theory, etc) and turn it into set theory you will invariably lose some of the intuition.
2. Structural set theory while able to serve basis for ZFC, make a crappy language to discuss a lot of the topics which do interest ZFC oriented set theorists. This is in a similar fashion of how ZFC make category theory cumbersome.

The discussions sort of faded out and died, but it seemed that they have went out with sort of a hint that type theory's day of the tentacle is nigh. In the form of Martin-Lof and SEAR/SEARC. But I don't know about that. I should stop. Thanks for reading.

-
There seems to be some misunderstanding going on here. No large cardinals are needed to develop the theory of model categories; in fact the very purpose of model category theory is to get rid of the need for universes in the study of abstract homotopy theory. It is true that Vopěnka's principle has some applications in model category theory (as well as category-theoretic model theory, which is a completely different subject), but that's kind of like saying that large cardinals have applications in point-set topology. –  Zhen Lin Feb 26 '13 at 17:15
@Zhen: Well to formalize in the syntactical sense you really just need something like PA. I read this as in the sense of "construct a model". And large cardinals do have applications in point-set topology. –  Asaf Karagila Feb 26 '13 at 17:24
There are plenty of interesting model categories that can be constructed in ordinary ZFC without the assistance of large cardinals. (Strange ones like StNaamen or whatever you're thinking of are probably not of interest to homotopy theorists.) –  Zhen Lin Feb 26 '13 at 17:27
@ZhenLin: StNaamen is not a model category, it's Qtficiation, QtNaamen is. But it only requires to start with a set model of ZFC, not the inaccessible that Misha and Assaf suggests in their paper. They also have some problems there which they ignore (regarding what are the actual objects of StNaamen). I pointed these to Misha during my work with him the last fall. I should really get to write that blog post about this. –  Asaf Karagila Feb 26 '13 at 17:39
@Zhen: I tried to mitigate the offensive part of the text, anyway. –  Asaf Karagila Feb 26 '13 at 17:49