# Is Frege's axiom of unrestricted comprehension actually true after all?

Consider the following demonstration whose first line is the assumption called the axiom of unrestricted comprehension.

1. ∀F∃y ∀x[x ∈ y iff F(x)] [OSC1]
2. ∀F∃y [α ∈ y iff F(α)] [UI]
3. ∃y [α ∈ y iff α ∉ α] [UI]
4. α ∈ x1 iff α ∉ α [EI]

The only way to get Russell's paradox is if alpha must be a general constant. But, in universal Instantiation, alpha is either a general constant or a specific constant. Therefore

1. ∀x[x=α] ∨ ∃! x[x=α]

If ∀x[x=α] then you get Russell's paradox. But you aren't done, because line 5 is a disjunction, so

1. ∃! x[x=α] [5; DS]

Thus alpha is a specific constant. If alpha equals x1 then you get Russell's paradox, so

1. x1 ≠ α

2. [α ∈ x1 iff α ∉ α] ∧ x1 ≠ α [4,7; conj]

3. ∀F∃y[α ∈ y iff F(α) ∧ y ≠ α]

Since alpha is a specific constant you can't universally generalize on it, you can only existentially generalize on it.

1. ∃x ∀F∃y[x ∈ y iff F(x) ∧ y ≠ x]

Closing the scope of the first assumption, line 1 implies line 10.

The point is, Russell's paradox is not a consequence of Gottlob Frege's axiom of unrestricted comprehension. This isn't surprising since Russell didn't understand the nuances of universal Instantiation in 1901. It wasn't until 1929 that Goedel proved the first order function calculus is complete, and I'm not sure if he knew the nuances of Universal Instantiation. In fact Leon Henkin's proof FOL is complete is the one I'm familiar with, and that proof came out in 1949. And it isn't clear to me that Henkin knew the nuances of Universal Instantiation either.

What do you think?

• Step 5 makes no sense. ∀x[x=α] says that your domain contains only a single value. ∃! x[x=α] is a consequence of the meaning of equivalence so it's always true for every value. Commented May 24 at 1:46
• Since Russell's paradox is not derived using the given argument, I'm not sure how fiddling with the given argument would suffice to rehabilitate unrestricted comprehension. Also, should we not be cautious about a claim that is tantamount to, "Set theorists hate this one weird trick!" since we would be claiming that somehow all mathematical logicians, including Frege himself, somehow missed out on this? Recall that Russell's paradox can be derived from restricted comprehension, e.g. separation, too, in the presence of a universal set. Something else is going on, isn't it? Commented May 24 at 4:05
• Even assuming that unrestricted comprehension does not derive Russell's paradox, how does that make it "true"? Plenty of things that do not derive contradictions are not true, and there are plenty of paradoxes besides Russell's. Commented May 24 at 4:31
• Regarding the puzzling statement: "since Russell didn't understand the nuances of universal Instantiation in 1901", see Bertrand Russell, Mathematical Logic as based on the Theory of Types (1908), II All and Any for the clear discussion of the interplay between Instantiation and Generalization. Commented May 24 at 9:53
• Your terms "specific constant" and "arbitrary constant" are not part of standard logic. A name can be a constant in which case it represents a specific single value from the domain or it can be a variable in which case it is implicitly universally quantified. If α is a constant, then ∀x[x=α] says that every value in the domain is equal to one specific value, α, which means that there is only one value, α, in the domain. If α is a variable then the formula is equivalent to ∀α∀x[x=α] which can only be true if the domain has one or fewer elements. Commented May 24 at 15:00

1. ∀F∃y ∀x[x ∈ y iff F(x)] [OSC1]
2. ∀F∃y [α ∈ y iff F(α)] [UI]
3. ∃y [α ∈ y iff α ∉ α] [UI]
4. α ∈ x1 iff α ∉ α [EI]

Step 2 is not how universal instantiation works. It only lets you remove the outermost ∀, but you're trying to use it on the innermost ∀. Here's a better version of what you're trying to do:

1. ∀F∃y ∀x[x ∈ y iff F(x)]
2. ∃y ∀x[x ∈ y iff x ∉ x] (UI, where F(x) is x ∉ x)
3. ∀x[x ∈ S iff x ∉ x] (EI, choosing the unused letter S)
4. S ∈ S iff S ∉ S (UI, substituting S for x).
• if there exists x, such that for any y[ P(x,y) ], then for any y there exists x, such that [ P(x,y)] so you can universally instantiate using the innermost universal quantifier. Your way requires you to instantiate F with an expression containing a variable, and I wanted to avoid that. But your line 4 doesn't follow from line 3 because in universal Instantiation, the constant you instantiate the variable with isn't necessarily a general constant, it's possible it's a specific constant. I'm using modal logic to understand this. Commented May 24 at 15:16
• @leepappas (1) "if there exists x, such that for any y[ P(x,y) ], then for any y there exists x, such that [ P(x,y)]" - this is true but the converse is not true; it is not the case that "if for any y there exists x such that P(x, y) implies there exists x such that for any y P(x, y)." By removing the innermost ∀ you are obtaining a weaker expression, not an equivalent one, which is why you have trouble reaching Russell's paradox afterwards. (2) Also even if it's valid it's just not the inference rule of UI: formally UI works on the outermost quantifier. Commented May 24 at 16:13
• (3) Line 4 does follow from line 3 by UI. UI in FOL doesn't care about modal logic. We're not using modal logic. Frege worked before modern modal logic. UI just allows you to replace ∀xA with A{x -> y}, where A{x -> y} is the result of replacing every free x variable in A with another variable y. There are no requirements on x or y. Commented May 24 at 16:15
• you need modal logic to understand universal Instantiation. Suppose you know for any x[P(x)]. That means P(x1)&P(x2)&P(x3)&.... You need to insist your Instantiation constant y is a general constant, to infer P(y). But that is a necessity condition which means you're using modal logic. It is possible that y is a specific constant. Thus you can't infer y is necessarily a general constant. Commented May 24 at 17:42
• @leepappas This distinction "general constant" or "specific constant" is not made in first order logic. Nor is there any concept of possible worlds. Commented May 24 at 17:48

There is a problem with representing the comprehension principle as a single axiom. It is more accurately read as an axiom scheme. So the specific formula that gives rise to the Russell set is an instance of, but not an inference from, the scheme; one cannot quite infer nonschematic sentences from schemes without going higher-order or into the land of proper class theory or whatnot, and then one is not quite working with the scheme anymore, anyway.

So at any rate, one need not represent the correlation between the general principle and the specific Russell-set instance as inferential, so the form of the given argument should not apply, here. There is no such erroneous universal instantiation going on, it would seem.

• There are two sorts of comprehension principle: the one that can be viewed as an axiom schema is the first-order principle that to any open formula there is a corresponding set. The question seems to be about the other sort of principle, the second-order axiom that to any predicate there corresponds a set. This second-order principle cannot be represented as an axiom schema. Commented May 24 at 7:54
• The modern type-theoretic way of putting this is that not every inhabited type's elements form a set; in a certain sense, sets are the smallest and simplest examples of types. Most active research on the topic involves homotopy levels, or h-levels (nLab, 1Lab); a set is a type with h-level 2. Commented May 24 at 23:39