Talk:Axiom schema of specification

Unrestricted comprehension and paradoxes

Concerning "unrestricted comprehension", PlanetMath's "comprehension axiom" says:

In theories which make no distinction between objects and sets (such as ZF), this formulation leads to Russel's paradox, however in stratified theories this is not a problem (for example second order arithmetic includes the axiom of comprehension).

This sounds correct to me (for a stratified theory, I'm thinking primarily of Russell and Whitehead's theory of types), but our article does not include this qualification, saying instead:

This axiom schema was tacitly used in the early days of naive set theory, before a strict axiomatisation was adopted. Unfortunately, it leads directly to Russell's paradox by taking P(C) to be (C is not in C). Therefore, no useful axiomatisation of set theory can use unrestricted comprehension, at least not with classical logic.

Can someone more knowledgeable than me reconcile the above, and edit the article appropriately. Paul August ☎ 21:20, 4 October 2005 (UTC)[reply]

I don't see any contradiction here. NF's comprehension axiom is not unrestricted;it's limited to stratified formulas. It's true that it uses urestricted quantification, but not what I'd call unrestricted comprehension. --Trovatore 21:27, 4 October 2005 (UTC)[reply]

Oh, you weren't talking about NF. Hmm. Well, second-order arithmetic isn't a (general) set theory, exactly. I'm really not all that familiar with the system of Principia. --Trovatore 21:30, 4 October 2005 (UTC)[reply]

Differences between this page and ZFC

The version on the ZFC page is different than the one on this page, and this page doesn't even list the version they have. I changed ZFC's to reflect this page's version, but it was quickly reverted. So I'm wondering if this page's version should instead be changed to the one ZFC has?

Nothing wrong with either version. All the ones on the ZFC page should probably pick one version consistently, but that doesn't mean this page should show only that version. Maybe, like axiom of choice, we could show many different versions.

Why are the w1, w2, ..., wn necessary

Let P be a predicate with free variables x, w₁, ..., w_n. Let's consider what happens for given values of the variables w₁, ..., w_n. There is a predicate Q(x) that is true exactly when P(x, w₁, ..., w_n) is true. For the first-order logic formula corresponding to the predicate Q, there is an axiom in the schema. So we don't need all these w₁, ..., w_n.

So I conclude that either:

there is something wrong with my logic
all the w* variables are not necessary in the definition of this axiom schema

If the first is true, then I think the article requires some clarification on that. Otherwise I really think we should remove all the w* variables from the definition for simplicity's sake. Martinkunev (talk) 23:30, 5 January 2014 (UTC)[reply]

I prefer a kind of logic in which formulas with free variables are considered meaningless (ambiguous). Every variable should be quantified (as in what some people call "free logic").

In any case, without the w variables there would only be a countable number of definable functions. With them there are an unlimited number of definable functions (if one replaces those variables with constants for elements of the model). JRSpriggs (talk) 05:44, 6 January 2014 (UTC)[reply]

I think I need to clarify what I mean.

\forall A\,\exists B\,\forall x\,(x\in B\Leftrightarrow [x\in A\land \varphi (x)])

What I'm trying to say is that this is an equivalent formula for an instance of the schema. — Preceding unsigned comment added by Martinkunev (talk • contribs) 23:58, 9 January 2014 (UTC)[reply]

If you are saying that limiting the schema to instances where the formula

\varphi \,

has only one free variable, namely x, is equivalent to the full power of the schema currently described in the article, then you are mistaken — it is much weaker. JRSpriggs (talk) 08:10, 10 January 2014 (UTC)[reply]