Definition df-clab 2705

Description: Define class abstractions, that is, classes of the form {𝑦 ∣ 𝜑}, which is read "the class of sets 𝑦 such that 𝜑(𝑦)".

A few remarks are in order:

1. The axiomatic statement df-clab 2705 does not define the class abstraction {𝑦 ∣ 𝜑} itself, that is, it does not have the form ⊢ {𝑦 ∣ 𝜑} = ... that a standard definition should have (for a good reason: equality itself has not yet been defined or axiomatized for class abstractions; it is defined later in df-cleq 2719). Instead, df-clab 2705 has the form ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ...), meaning that it only defines what it means for a setvar to be a member of a class abstraction. As a consequence, one can say that df-clab 2705 defines class abstractions if and only if a class abstraction is completely determined by which elements belong to it, which is the content of the axiom of extensionality ax-ext 2698. Therefore, df-clab 2705 can be considered a definition only in systems that can prove ax-ext 2698 (and the necessary first-order logic).

2. As in all definitions, the definiendum (the left-hand side of the biconditional) has no disjoint variable conditions. In particular, the setvar variables 𝑥 and 𝑦 need not be distinct, and the formula 𝜑 may depend on both 𝑥 and 𝑦. This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on 𝑥, 𝑦, then one could not do anything with expressions like 𝑥 ∈ {𝑥 ∣ 𝜑} which are sometimes useful to shorten proofs (because of abid 2708). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑.

3. Remark 1 stresses that df-clab 2705 does not have the standard form of a definition for a class, but one could be led to think it has the standard form of a definition for a formula. However, it also fails that test since the membership predicate ∈ has already appeared earlier (outside of syntax e.g. in ax-8 2101). Indeed, the definiendum extends, or "overloads", the membership predicate ∈ from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is possible because of wcel 2099 and cab 2704, and it can be called an "extension" of the membership predicate because of wel 2100, whose proof uses cv 1533. An a posteriori justification for cv 1533 is given by cvjust 2721, stating that every setvar can be written as a class abstraction (though conversely not every class abstraction is a set, as illustrated by Russell's paradox ru 3773).

4. Proof techniques. Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable. This is done with theorems such as vtoclg 3538 which is used, for example, to convert elirrv 9611 to elirr 9612.

5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2705, df-cleq 2719, and df-clel 2805, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30197), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2719 and df-clel 2805). One could be less strict and decide to call "definition" every axiomatic statement which provides an eliminable and conservative extension of the considered axiom system. But the notion of conservativity may be given two different meanings in set.mm, due to the difference between the "scheme level" of set.mm and the "object level" of classical treatments. For a proof that these three axiomatic statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ax-ext 2698, see Appendix of [Levy] p. 357.

6. References and history. The concept of class abstraction dates back to at least Frege, and is used by Whitehead and Russell. This definition is Definition 2.1 of [Quine] p. 16 and Axiom 4.3.1 of [Levy] p. 12. It is called the "axiom of class comprehension" by [Levy] p. 358, who treats the theory of classes as an extralogical extension to predicate logic and set theory axioms. He calls the construction {𝑦 ∣ 𝜑} a "class term". For a full description of how classes are introduced and how to recover the primitive language, see the books of Quine and Levy (and the comment of eqabb 2868 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2868. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)

Assertion

Ref	Expression
df-clab	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2	1	cv 1533	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2704	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2099	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 2060	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 205	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  eleq1ab  2706  abid  2708  vexwt  2709  vexw  2710  nfsab1  2712  hbab1OLD  2714  hbab  2715  hbabg  2716  cvjust  2721  abbi  2795  abbib  2799  cbvabv  2800  cbvabw  2801  cbvabwOLD  2802  cbvab  2803  eqabbw  2804  eqabdv  2862  clelab  2874  clelabOLD  2875  nfabdw  2921  nfabdwOLD  2922  nfabd  2923  rabrabi  3445  abv  3480  abvALT  3481  elab6g  3655  elrabi  3674  ralab  3684  dfsbcq2  3777  sbc8g  3782  sbcimdv  3847  sbcg  3852  csbied  3927  ss2abdv  4056  ss2abdvALT  4057  unabw  4293  unab  4294  inab  4295  difab  4296  notabw  4299  noel  4326  noelOLD  4327  vn0  4334  eq0  4339  ab0w  4369  ab0OLD  4371  ab0orv  4374  eq0rdv  4400  csbab  4433  disj  4443  rzal  4504  ralf0  4509  exss  5459  iotaeq  6507  abrexex2g  7962  opabex3d  7963  opabex3rd  7964  opabex3  7965  xpab  35256  eliminable1  36272  eliminable-velab  36278  bj-ab0  36322  bj-elabd2ALT  36339  bj-gabima  36354  bj-snsetex  36378  wl-clabv  36997  wl-clabtv  36999  wl-clabt  37000  ss2ab1  41627  elabgw  42012  scottabf  43600

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »