Axiom:Axiom of Specification/Class Theory

From ProofWiki
Jump to navigation Jump to search


It has been suggested that this page be renamed.
In particular: This page and its redirect should specify that we're talking NBG set theory
To discuss this page in more detail, feel free to use the talk page.


Axiom

The Axiom of Specification is an axiom schema which can be formally stated as follows:


Let $\map \phi {A_1, A_2, \ldots, A_n, x}$ be a propositional function such that:

$A_1, A_2, \ldots, A_n$ are a finite number of free variables whose domain ranges over all classes
$x$ is a free variable whose domain ranges over all sets


Then the Axiom of Specification gives that:

$\forall A_1, A_2, \ldots, A_n: \exists B: \forall x: \paren {x \in B \iff \map \phi {A_1, A_2, \ldots, A_n, x} }$

where each of $B$ ranges over arbitrary classes.


This means that for any finite number $A_1, A_2, \ldots, A_n$ of subclasses of the universal class $V$, the class $B$ exists (or can be formed) of all sets $x \in V$ that satisfy the function $\map \phi {A_1, A_2, \ldots, A_n, x}$.


This page or section has statements made on it that ought to be extracted and proved in a Theorem page.
In particular: The following is digression which needs to be removed from here and put into its own page.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by creating any appropriate Theorem pages that may be needed.
To discuss this page in more detail, feel free to use the talk page.


Allowing bound proper class variables to be hidden inputs for $\phi$ results in Morse-Kelley set theory, which is strictly stronger than Gödel-Bernays set theory.


Also known as

The Axiom of Specification is also known as:

  • The Axiom of Subsets (although this unnecessarily reduces the scope of this axiom to pure set theory)
  • The Axiom of Comprehension
  • The Axiom of Selection (this axiom allows one to select the elements of a subset)
  • The Axiom of Separation or Separation Principle (although this can be confused with the Tychonoff separation axioms, which arise in topology, so this name is deprecated on $\mathsf{Pr} \infty \mathsf{fWiki}$)
  • The Axiom of Segregation, under its German name Aussonderungsaxiom
  • The limited abstraction principle, in apposition to the unlimited abstraction principle, also known as the axiom of abstraction.
  • In the context of class theory, the term Axiom of Class Formation is often seen.


Also see


Historical Note

The Axiom of Specification was created by Ernst Zermelo as a replacement for the Axiom of Abstraction of Frege set theory.

The latter had been demonstrated, via Russell's Paradox, to lead to the conclusion that Frege Set Theory is Logically Inconsistent.

Thus, rather than allowing a set to be constructed of any elements at all which satisfy a given property $P$, the elements in question are restricted to being elements of some pre-existing set.

This in turn leads to the further question of how to create such a pre-existing set in the first place.

Hence the need to develop further axioms in order to allow the creation of such sets.

As a result of this, Ernst Zermelo found it necessary to create:

the Axiom of the Empty Set, allowing for the existence of $\O := \set {}$
the Axiom of Pairing, allowing for $\set {a, b}$ given the existence of $a$ and $b$
the Axiom of Unions, allowing for $\bigcup a$ given the existence of a set $a$ of sets
the Axiom of Powers, allowing for the power set $\powerset a$ to be generated for any set $a$
the Axiom of Infinity, allowing for the creation of the set of natural numbers $\N$.


Internationalization

Axiom of Specification is translated:

In German: Aussonderungsaxiom  (literally: axiom of segregation)


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Axiom:Axiom_of_Specification/Class_Theory&oldid=589704"