Originally Posted by

**Angra Mainyu**
I think I'm probably not getting the notation, but what I was trying to get at is something like this: We are using AC (if we don't have AC, one can make other arguments), so every set has a cardinality. Suppose that Y is a set of propositions with cardinality a, and let b be the next cardinal. For every cardinal c<=b such that c=\=a, let P(c) be the proposition "It is not the case that the cardinality of Y is c", and let P(a) be the proposition "The cardinality of Y is a". Then, for all c<=b, P(c) is a true proposition, and at least one of those true propositions is not an element of Y (else, we would have a>=c, contradicting the hypothesis). Thus, there is no set of all true propositions.

Yes. Sets of propositions would either need to be suitably stratified or an impredicative class. But we can sidestep this and only consider subsets of the finite set X = {T, everything holds}. So long as X can be admitted to exist, we go with

Code:

1) Consider the subset of X consisting of propositions Q such that P or Q. This is non-empty since it at least contains T.
2) Consider the subset of X consisting of propositions R such that either P or else (R implies everything). This is non-empty since it at least contains the proposition "everything holds".