2 added 38 characters in body

Let me restrict and better formalize this question to ask, "If we have some first-order formula $\varphi(x)$ expressible (with parameters) in the language of set theory, when will $\lnot \exists x \varphi(x)$ be true?" In other words, when will we have an object that cannot exist as a set when sufficiently described? For example, the question of whether the class of all sets is proper is equivalent to the question of whether $\lnot \exists x \varphi(x)$ where $\varphi(x) \equiv \forall y(y \in x)$. Since this statement is easily provable in ZFC, we say that the class of all sets is indeed proper. As another example, we can consider the existence of a generic filter for some partial order as mentioned by Adam. In this case, we could fix a partial order $\mathbb{P}$ and have $\varphi(x)$ be the statement "$x$ is a filter on $\mathbb{P}$ intersecting all dense subsets of $\mathbb{P}$.'' There may be many such $x$ external to the universe that satisfy these criteria, but if $\mathbb{P}$ is a nontrivial forcing notion such as the forcing to add a Cohen Real, we will be able to prove $\lnot \exists x \varphi(x)$ so that any such filter $x$ cannot be a set in the universe. Thus any such generic object must be a proper class.

In this sense, I would characterize a class as being proper when its existence as an object in the universe would cause set theory to be inconsistent. Since we consider a wide variety of models in set theory today (some which may even be sets themselves), I would argue that "too big" is a somewhat outdated intuition for characterizing all proper classes that can arise. For example, if we consider a countable model $M$ of ZFC, we can force to add a wide variety of sets to it that are proper classes of $M$. Also, if $0^{\sharp}$ (a Real number encoding truth in $L$) exists, then this will be a proper class of the constructible universe $L$ containing all ordinals. I therefore claim that a proper class is merely an object that reveals too much about the universe in question to be a set in this universe.

In light of these considerations, I would always consider proper classes in terms of specific models of a theory. In this sense, proper classes are ubiquitous. For example, the set of all primes in any model of Peano arithmetic would be a proper class in the context of this model. Pure mathematicians may need to consider such questions about proper classes of models in proofs. For example, when Andrew Wiles proved Fermat's Last Theorem, he appealed to the existence of a Grothendieck universe, which is a proper class of any set-theoretic universe without an inaccessible cardinal. Since we cannot even prove the consistency of the existence of such a cardinal in ZFC, a mathematician should be aware that he/she may be appealing to a stronger theory than set theory alone when assuming that Fermat's Last Theorem is true (although the discussion on http://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof seems to suggest this large cardinal assumption was inessential). As Greg pointed out, it may be sufficient to only consider universes with an inaccessible cardinal for most mathematics thereby eliminating the need to consider proper classes. However, one never knows when a new theorem may rely on the use of large cardinals with even greater consistency strength. For example, there is a result in category theory appealing to the existence of a cardinal with very large consistency strength (Vopěnka's Principle). There are also proper class considerations to be made in determining whether it even makes sense to talk about a conjecture. (i.e., is it formalizable in the language?)

Finally, as a point of clarification to Greg's post, $\aleph_0$ is technically not an inaccessible cardinal under the standard definition I'm accustomed to, which requires the cardinal to be uncountable. The reason for this is because inaccessibility is considered a large cardinal notion, which whose consistency should always be independent of ZFC. Since the (consistency of the) existence of $\aleph_0$ is provable from ZFC, it should not be characterized as a large cardinal. However, as noted, it could be considered a large cardinal in the absence of the axiom of infinity.

1

Let me restrict and better formalize this question to ask, "If we have some first-order formula $\varphi(x)$ expressible (with parameters) in the language of set theory, when will $\lnot \exists x \varphi(x)$ be true?" In other words, when will we have an object that cannot exist as a set when sufficiently described? For example, the question of whether the class of all sets is proper is equivalent to the question of whether $\lnot \exists x \varphi(x)$ where $\varphi(x) \equiv \forall y(y \in x)$. Since this statement is easily provable in ZFC, we say that the class of all sets is indeed proper. As another example, we can consider the existence of a generic filter for some partial order as mentioned by Adam. In this case, we could fix a partial order $\mathbb{P}$ and have $\varphi(x)$ be the statement "$x$ is a filter on $\mathbb{P}$ intersecting all dense subsets of $\mathbb{P}$.'' There may be many such $x$ external to the universe that satisfy these criteria, but if $\mathbb{P}$ is a nontrivial forcing notion such as the forcing to add a Cohen Real, we will be able to prove $\lnot \exists x \varphi(x)$ so that any such filter $x$ cannot be a set in the universe. Thus any such generic object must be a proper class.

In this sense, I would characterize a class as being proper when its existence as an object in the universe would cause set theory to be inconsistent. Since we consider a wide variety of models in set theory today (some which may even be sets themselves), I would argue that "too big" is a somewhat outdated intuition for characterizing all proper classes that can arise. For example, if we consider a countable model $M$ of ZFC, we can force to add a wide variety of sets to it that are proper classes of $M$. Also, if $0^{\sharp}$ (a Real number encoding truth in $L$) exists, then this will be a proper class of the constructible universe $L$ containing all ordinals. I therefore claim that a proper class is merely an object that reveals too much about the universe in question to be a set in this universe.

In light of these considerations, I would always consider proper classes in terms of specific models of a theory. In this sense, proper classes are ubiquitous. For example, the set of all primes in any model of Peano arithmetic would be a proper class in the context of this model. Pure mathematicians may need to consider such questions in proofs. For example, when Andrew Wiles proved Fermat's Last Theorem, he appealed to the existence of a Grothendieck universe, which is a proper class of any set-theoretic universe without an inaccessible cardinal. Since we cannot even prove the consistency of the existence of such a cardinal in ZFC, a mathematician should be aware that he/she may be appealing to a stronger theory than set theory alone when assuming that Fermat's Last Theorem is true (although the discussion on http://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof seems to suggest this large cardinal assumption was inessential). As Greg pointed out, it may be sufficient to only consider universes with an inaccessible cardinal for most mathematics thereby eliminating the need to consider proper classes. However, one never knows when a new theorem may rely on the use of large cardinals with even greater consistency strength. For example, there is a result in category theory appealing to the existence of a cardinal with very large consistency strength (Vopěnka's Principle). There are also proper class considerations to be made in determining whether it even makes sense to talk about a conjecture. (i.e., is it formalizable in the language?)

Finally, as a point of clarification to Greg's post, $\aleph_0$ is technically not an inaccessible cardinal under the standard definition I'm accustomed to, which requires the cardinal to be uncountable. The reason for this is because inaccessibility is considered a large cardinal notion, which should always be independent of ZFC. Since the (consistency of the) existence of $\aleph_0$ is provable from ZFC, it should not be characterized as a large cardinal. However, as noted, it could be considered a large cardinal in the absence of the axiom of infinity.