Фон Нейман - Бернейс - Гёдель теория набора

В математики основе фон Нейман - Бернейс -Гёдель Теория набора ( NBG ) является аксиоматической теорией , которая является консервативным расширением теории набора Zermelo -Fraenkel -Choice (ZFC). NBG представляет понятие класса определяемых , которое представляет собой набор наборов, формулой , которых квантификаторы только по наборам. NBG может определять классы, которые больше, чем набор, такие как класс всех наборов и класс всех ординалов . Теория наборов Морс -Келли (MK) позволяет определять классы формулами, квантовые показатели которых в диапазоне по классам. NBG конечно аксиоматизируется, а ZFC и MK - нет.

Ключевой теоремой NBG является теорема существования классов, которая утверждает, что для каждой формулы, кванторы которой распространяются только на множества, существует класс, состоящий из множеств, удовлетворяющих этой формуле. Этот класс построен путем отражения пошагового построения формулы с помощью классов. Поскольку все теоретико-множественные формулы строятся из двух видов атомарных формул ( членства и равенства ) и конечного числа логических символов , лишь конечное число аксиом для построения удовлетворяющих им классов требуется . Вот почему NBG конечно аксиоматизируем. Классы также используются для других конструкций, для обработки теоретико-множественных парадоксов и для формулировки аксиомы глобального выбора ZFC , которая более сильная, чем аксиома выбора .

Джон фон Нейман ввел классы в теорию множеств в 1925 году. Примитивными понятиями его теории были функция и аргумент . Используя эти понятия, он определил класс и множество. Пауль Бернейс переформулировал теорию фон Неймана, приняв класс и множество как примитивные понятия. Курт Гёдель упростил теорию Бернейса для относительной непротиворечивости доказательства аксиомы выбора и гипотезы обобщенного континуума .

Classes in set theory

The uses of classes

Classes have several uses in NBG:

• They produce a finite axiomatization of set theory.
• They are used to state a "very strong form of the axiom of choice"—namely, the axiom of global choice: There exists a global choice function $G$ defined on the class of all nonempty sets such that $G(x)\in x$ for every nonempty set $x.$ This is stronger than ZFC's axiom of choice: For every set $s$ of nonempty sets, there exists a choice function $f$ defined on $s$ such that $f(x)\in x$ for all $x\in s.$
• The set-theoretic paradoxes are handled by recognizing that some classes cannot be sets. For example, assume that the class $Ord$ of all ordinals is a set. Then $Ord$ is a transitive set well-ordered by $\in$. So, by definition, $Ord$ is an ordinal. Hence, $Ord\in Ord$, which contradicts $\in$ being a well-ordering of $Ord.$ Therefore, $Ord$ is not a set. A class that is not a set is called a proper class; $Ord$ is a proper class.
• Proper classes are useful in constructions. In his proof of the relative consistency of the axiom of global choice and the generalized continuum hypothesis, Gödel used proper classes to build the constructible universe. He constructed a function on the class of all ordinals that, for each ordinal, builds a constructible set by applying a set-building operation to previously constructed sets. The constructible universe is the image of this function.

Axiom schema versus class existence theorem

Once classes are added to the language of ZFC, it is easy to transform ZFC into a set theory with classes. First, the axiom schema of class comprehension is added. This axiom schema states: For every formula $\phi (x_{1},\ldots ,x_{n})$ that quantifies only over sets, there exists a class $A$ consisting of the $n$-tuples satisfying the formula—that is, $\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n})].$ Then the axiom schema of replacement is replaced by a single axiom that uses a class. Finally, ZFC's axiom of extensionality is modified to handle classes: If two classes have the same elements, then they are identical. The other axioms of ZFC are not modified.

This theory is not finitely axiomatized. ZFC's replacement schema has been replaced by a single axiom, but the axiom schema of class comprehension has been introduced.

To produce a theory with finitely many axioms, the axiom schema of class comprehension is first replaced with finitely many class existence axioms. Then these axioms are used to prove the class existence theorem, which implies every instance of the axiom schema. The proof of this theorem requires only seven class existence axioms, which are used to convert the construction of a formula into the construction of a class satisfying the formula.

Axiomatization of NBG

Classes and sets

NBG has two types of objects: classes and sets. Intuitively, every set is also a class. There are two ways to axiomatize this. Bernays used many-sorted logic with two sorts: classes and sets. Gödel avoided sorts by introducing primitive predicates: ${\mathfrak {Cls}}(A)$ for "$A$ is a class" and ${\mathfrak {M}}(A)$ for "$A$ is a set" (in German, "set" is Menge). He also introduced axioms stating that every set is a class and that if class $A$ is a member of a class, then $A$ is a set. Using predicates is the standard way to eliminate sorts. Elliott Mendelson modified Gödel's approach by having everything be a class and defining the set predicate $M(A)$ as $\exists C(A\in C).$ This modification eliminates Gödel's class predicate and his two axioms.

Bernays' two-sorted approach may appear more natural at first, but it creates a more complex theory. In Bernays' theory, every set has two representations: one as a set and the other as a class. Also, there are two membership relations: the first, denoted by "∈", is between two sets; the second, denoted by "η", is between a set and a class. This redundancy is required by many-sorted logic because variables of different sorts range over disjoint subdomains of the domain of discourse.

The differences between these two approaches do not affect what can be proved, but they do affect how statements are written. In Gödel's approach, $A\in C$ where $A$ and $C$ are classes is a valid statement. In Bernays' approach this statement has no meaning. However, if $A$ is a set, there is an equivalent statement: Define "set $a$ represents class $A$" if they have the same sets as members—that is, $\forall x(x\in a\iff x\;\eta \;A).$ The statement $a\;\eta \;C$ where set $a$ represents class $A$ is equivalent to Gödel's $A\in C.$

The approach adopted in this article is that of Gödel with Mendelson's modification. This means that NBG is an axiomatic system in first-order predicate logic with equality, and its only primitive notions are class and the membership relation.

Definitions and axioms of extensionality and pairing

A set is a class that belongs to at least one class: $A$ is a set if and only if $\exists C(A\in C)$. A class that is not a set is called a proper class: $A$ is a proper class if and only if $\forall C(A\notin C)$. Therefore, every class is either a set or a proper class, and no class is both.

Gödel introduced the convention that uppercase variables range over classes, while lowercase variables range over sets. Gödel also used names that begin with an uppercase letter to denote particular classes, including functions and relations defined on the class of all sets. Gödel's convention is used in this article. It allows us to write:

• $\exists x\,\phi (x)$ instead of $\exists x{\bigl (}\exists C(x\in C)\land \phi (x){\bigr )}$
• $\forall x\,\phi (x)$ instead of $\forall x{\bigl (}\exists C(x\in C)\implies \phi (x){\bigr )}$

The following axioms and definitions are needed for the proof of the class existence theorem.

Axiom of extensionality.  If two classes have the same elements, then they are identical.

$\forall A\,\forall B\,[\forall x(x\in A\iff x\in B)\implies A=B]$ 

This axiom generalizes ZFC's axiom of extensionality to classes.

Axiom of pairing.  If $x$ and $y$ are sets, then there exists a set $p$ whose only members are $x$ and $y$.

$\forall x\,\forall y\,\exists p\,\forall z\,[z\in p\iff (z=x\,\lor \,z=y)]$ 

As in ZFC, the axiom of extensionality implies the uniqueness of the set $p$, which allows us to introduce the notation $\{x,y\}.$

Ordered pairs are defined by:

$(x,y)=\{\{x\},\{x,y\}\}$

Tuples are defined inductively using ordered pairs:

$(x_{1})=x_{1},$

${\text{For }}n>1\!:(x_{1},\ldots ,x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-1}),x_{n}).$

Class existence axioms and axiom of regularity

Class existence axioms will be used to prove the class existence theorem: For every formula in $n$ free set variables that quantifies only over sets, there exists a class of $n$-tuples that satisfy it. The following example starts with two classes that are functions and builds a composite function. This example illustrates the techniques that are needed to prove the class existence theorem, which lead to the class existence axioms that are needed.

Example 1:  If the classes $F$ and $G$ are functions, then the composite function $G\circ F$ is defined by the formula: $\exists t[(x,t)\in F\,\land \,(t,y)\in G].$ Since this formula has two free set variables, $x$ and $y,$ the class existence theorem constructs the class of ordered pairs: $G\circ F\,=\,\{(x,y):\exists t[(x,t)\in F\,\land \,(t,y)\in G]\}.$ Because this formula is built from simpler formulas using conjunction $\land$ and existential quantification $\exists$, class operations are needed that take classes representing the simpler formulas and produce classes representing the formulas with $\land$ and $\exists$. To produce a class representing a formula with $\land$, intersection used since $x\in A\cap B\iff x\in A\land x\in B.$ To produce a class representing a formula with $\exists$, the domain is used since $x\in Dom(A)\iff \exists t[(x,t)\in A].$ Before taking the intersection, the tuples in $F$ and $G$ need an extra component so they have the same variables. The component $y$ is added to the tuples of $F$ and $x$ is added to the tuples of $G$: $$F'=\{(x,t,y):(x,t)\in F\}\,$$ and $\,G'=\{(t,y,x):(t,y)\in G\}$ In the definition of $F',$ the variable $y$ is not restricted by the statement $(x,t)\in F,$ so $y$ ranges over the class $V$ of all sets. Similarly, in the definition of $G',$ the variable $x$ ranges over $V.$ So an axiom is needed that adds an extra component (whose values range over $V$) to the tuples of a given class. Next, the variables are put in the same order to prepare for the intersection: $$F''=\{(x,y,t):(x,t)\in F\}\,$$ and $\,G''=\{(x,y,t):(t,y)\in G\}$ To go from $F'$ to $F''$ and from $G'$ to $G''$ requires two different permutations, so axioms that support permutations of tuple components are needed. The intersection of $F''$ and $G''$ handles $\land$: $$F''\cap G''=\{(x,y,t):(x,t)\in F\,\land \,(t,y)\in G\}$$ Since $(x,y,t)$ is defined as $((x,y),t)$, taking the domain of $F''\cap G''$ handles $\exists t$ and produces the composite function: $$G\circ F=Dom(F''\cap G'')=\{(x,y):\exists t((x,t)\in F\,\land \,(t,y)\in G)\}$$ So axioms of intersection and domain are needed.

The class existence axioms are divided into two groups: axioms handling language primitives and axioms handling tuples. There are four axioms in the first group and three axioms in the second group.

Axioms for handling language primitives:

Membership.  There exists a class $E$ containing all the ordered pairs whose first component is a member of the second component.

$\exists E\,\forall x\,\forall y\,[(x,y)\in E\iff x\in y]\!$ 

Intersection (conjunction).  For any two classes $A$ and $B$, there is a class $C$ consisting precisely of the sets that belong to both $A$ and $B$.

$\forall A\,\forall B\,\exists C\,\forall x\,[x\in C\iff (x\in A\,\land \,x\in B)]$ 

Complement (negation).  For any class $A$, there is a class $B$ consisting precisely of the sets not belonging to $A$.

$\forall A\,\exists B\,\forall x\,[x\in B\iff \neg (x\in A)]$ 

Domain (existential quantifier).  For any class $A$, there is a class $B$ consisting precisely of the first components of the ordered pairs of $A$.

$\forall A\,\exists B\,\forall x\,[x\in B\iff \exists y((x,y)\in A)]$ 

By the axiom of extensionality, class $C$ in the intersection axiom and class $B$ in the complement and domain axioms are unique. They will be denoted by: $A\cap B,$ $\complement A,$ and $Dom(A),$ respectively.

The first three axioms imply the existence of the empty class and the class of all sets: The membership axiom implies the existence of a class $E.$ The intersection and complement axioms imply the existence of $E\cap \complement E$, which is empty. By the axiom of extensionality, this class is unique; it is denoted by $\emptyset .$ The complement of $\emptyset$ is the class $V$ of all sets, which is also unique by extensionality. The set predicate $M(A)$, which was defined as $\exists C(A\in C)$, is now redefined as $A\in V$ to avoid quantifying over classes.

Axioms for handling tuples:

Product by $V$.  For any class $A$, there is a class $B$ consisting of the ordered pairs whose first component belongs to $A$.

$\forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A)]$

Circular permutation.  For any class $A$, there is a class $B$ whose 3‑tuples are obtained by applying the circular permutation $(y,z,x)\mapsto (x,y,z)$ to the 3‑tuples of $A$.

$\forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (y,z,x)\in A]$

Transposition.  For any class $A$, there is a class $B$ whose 3‑tuples are obtained by transposing the last two components of the 3‑tuples of $A$.

$\forall A\,\exists B\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B\iff (x,z,y)\in A]$

By extensionality, the product by $V$ axiom implies the existence of a unique class, which is denoted by $A\times V.$ This axiom is used to define the class $V^{n}$ of all $n$-tuples: $V^{1}=V$ and $V^{n+1}=V^{n}\times V.\,$ If $A$ is a class, extensionality implies that $A\cap V^{n}$ is the unique class consisting of the $n$-tuples of $A.$ For example, the membership axiom produces a class $E$ that may contain elements that are not ordered pairs, while the intersection $E\cap V^{2}$ contains only the ordered pairs of $E$.

The circular permutation and transposition axioms do not imply the existence of unique classes because they specify only the 3‑tuples of class $B.$ By specifying the 3‑tuples, these axioms also specify the $n$-tuples for $n\geq 4$ since: $$(x_{1},\ldots ,x_{n-2},x_{n-1},x_{n})=((x_{1},\ldots ,x_{n-2}),x_{n-1},x_{n}).$$ The axioms for handling tuples and the domain axiom imply the following lemma, which is used in the proof of the class existence theorem.

Tuple lemma — 

1. $$\forall A\,\exists B_{1}\,\forall x\,\forall y\,\forall z\,[(z,x,y)\in B_{1}\iff (x,y)\in A]$$
2. $$\forall A\,\exists B_{2}\,\forall x\,\forall y\,\forall z\,[(x,z,y)\in B_{2}\iff (x,y)\in A]$$
3. $$\forall A\,\exists B_{3}\,\forall x\,\forall y\,\forall z\,[(x,y,z)\in B_{3}\iff (x,y)\in A]$$
4. $$\forall A\,\exists B_{4}\,\forall x\,\forall y\,\forall z\,[(y,x)\in B_{4}\iff (x,y)\in A]$$

Proof

• Class $B_{3}$: Apply product by $V$ to $A$ to produce $B_{3}.$
• Class $B_{2}$: Apply transposition to $B_{3}$ to produce $B_{2}.$
• Class $B_{1}$: Apply circular permutation to $B_{3}$ to produce $B_{1}.$
• Class $B_{4}$: Apply circular permutation to $B_{2}$, then apply domain to produce $B_{4}.$

One more axiom is needed to prove the class existence theorem: the axiom of regularity. Since the existence of the empty class has been proved, the usual statement of this axiom is given.

Axiom of regularity.  Every nonempty set has at least one element with which it has no element in common. $$\forall a\,[a\neq \emptyset \implies \exists u(u\in a\land u\cap a=\emptyset )].$$

This axiom implies that a set cannot belong to itself: Assume that $x\in x$ and let $a=\{x\}.$ Then $x\cap a\neq \emptyset$ since $x\in x\cap a.$ This contradicts the axiom of regularity because $x$ is the only element in $a.$ Therefore, $x\notin x.$ The axiom of regularity also prohibits infinite descending membership sequences of sets: $$\cdots \in x_{n+1}\in x_{n}\in \cdots \in x_{1}\in x_{0}.$$

Gödel stated regularity for classes rather than for sets in his 1940 monograph, which was based on lectures given in 1938. In 1939, he proved that regularity for sets implies regularity for classes.

Class existence theorem

Class existence theorem — Let $\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})$ be a formula that quantifies only over sets and contains no free variables other than $x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}$ (not necessarily all of these). Then for all $Y_{1},\dots ,Y_{m}$, there exists a unique class $A$ of $n$-tuples such that: $$\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})].$$ The class $A$ is denoted by $\{(x_{1},\dots ,x_{n}):\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})\}.$

The theorem's proof will be done in two steps:

1. Transformation rules are used to transform the given formula $\phi$ into an equivalent formula that simplifies the inductive part of the proof. For example, the only logical symbols in the transformed formula are $\neg$, $\land$, and $\exists$, so the induction handles logical symbols with just three cases.
2. The class existence theorem is proved inductively for transformed formulas. Guided by the structure of the transformed formula, the class existence axioms are used to produce the unique class of $n$-tuples satisfying the formula.

Transformation rules.  In rules 1 and 2 below, $\Delta$ and $\Gamma$ denote set or class variables. These two rules eliminate all occurrences of class variables before an $\in$ and all occurrences of equality. Each time rule 1 or 2 is applied to a subformula, $i$ is chosen so that $z_{i}$ differs from the other variables in the current formula. The three rules are repeated until there are no subformulas to which they can be applied. This produces a formula that is built only with $\neg$, $\land$, $\exists$, $\in$, set variables, and class variables $Y_{k}$ where $Y_{k}$ does not appear before an $\in$.

1. $\,Y_{k}\in \Gamma$ is transformed into $\exists z_{i}(z_{i}=Y_{k}\,\land \,z_{i}\in \Gamma ).$
2. Extensionality is used to transform $\Delta =\Gamma$ into $\forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ).$
3. Logical identities are used to transform subformulas containing $\lor ,\implies ,\iff ,$ and $\forall$ to subformulas that only use $\neg ,\land ,$ and $\exists .$

Transformation rules: bound variables.  Consider the composite function formula of example 1 with its free set variables replaced by $x_{1}$ and $x_{2}$: $\exists t[(x_{1},t)\in F\,\land \,(t,x_{2})\in G].$ The inductive proof will remove $\exists t$, which produces the formula $(x_{1},t)\in F\land (t,x_{2})\in G.$ However, since the class existence theorem is stated for subscripted variables, this formula does not have the form expected by the induction hypothesis. This problem is solved by replacing the variable $t$ with $x_{3}.$ Bound variables within nested quantifiers are handled by increasing the subscript by one for each successive quantifier. This leads to rule 4, which must be applied after the other rules since rules 1 and 2 produce quantified variables.

4. If a formula contains no free set variables other than $x_{1},\dots ,x_{n},$ then bound variables that are nested within $q$ quantifiers are replaced with $x_{n+q}$. These variables have (quantifier) nesting depth $q$.

Example 2:  Rule 4 is applied to the formula $\phi (x_{1})$ that defines the class consisting of all sets of the form $\{\emptyset ,\{\emptyset ,\dots \},\dots \}.$ That is, sets that contain at least $\emptyset$ and a set containing $\emptyset$ — for example, $\{\emptyset ,\{\emptyset ,a,b,c\},d,e\}$ where $a,b,c,d,$ and $e$ are sets. $${\begin{aligned}\phi (x_{1})\,&=\,\exists u\;\,[\,u\in x_{1}\,\land \,\neg \exists v\;\,(\;v\,\in \,u\,)]\,\land \,\,\exists w\;{\bigl (}w\in x_{1}\,\land \,\exists y\;\,[(\;y\,\in w\;\land \;\neg \exists z\;\,(\;z\,\in \,y\,)]{\bigr )}\\\phi _{r}(x_{1})\,&=\,\exists x_{2}[x_{2}\!\in \!x_{1}\,\land \,\neg \exists x_{3}(x_{3}\!\in \!x_{2})]\,\land \,\,\exists x_{2}{\bigl (}x_{2}\!\in \!x_{1}\,\land \,\exists x_{3}[(x_{3}\!\in \!x_{2}\,\land \,\neg \exists x_{4}(x_{4}\!\in \!x_{3})]{\bigr )}\end{aligned}}$$ Since $x_{1}$ is the only free variable, $n=1.$ The quantified variable $x_{3}$ appears twice in $x_{3}\in x_{2}$ at nesting depth 2. Its subscript is 3 because $n+q=1+2=3.$ If two quantifier scopes are at the same nesting depth, they are either identical or disjoint. The two occurrences of $x_{3}$ are in disjoint quantifier scopes, so they do not interact with each other.

Proof of the class existence theorem.  The proof starts by applying the transformation rules to the given formula to produce a transformed formula. Since this formula is equivalent to the given formula, the proof is completed by proving the class existence theorem for transformed formulas.

Proof of the class existence theorem for transformed formulas

The following lemma is used in the proof.

Expansion lemma — Let $1\leq i<j\leq n,$ and let $P$ be a class containing all the ordered pairs $(x_{i},x_{j})$ satisfying $R(x_{i},x_{j}).$ That is, $P\supseteq \{(x_{i},x_{j}):R(x_{i},x_{j})\}.$ Then $P$ can be expanded into the unique class $Q$ of $n$-tuples satisfying $R(x_{i},x_{j})$. That is, $Q=\{(x_{1},\ldots ,x_{n}):R(x_{i},x_{j})\}.$

Proof:

1. If $i=1,$ let $P_{1}=P.$
   Otherwise, $i>1,$ so components are added in front of $x_{i}{\text{:}}$ apply the tuple lemma's statement 1 to $P$ with $z=(x_{1},\dots ,x_{i-1}).$ This produces a class $P_{1}$ containing all the $(i+1)$-tuples $$((x_{1},\dots ,x_{i-1}),x_{i},x_{j})=(x_{1},\dots ,x_{i-1},x_{i},x_{j})$$ satisfying $R(x_{i},x_{j}).$
2. If $j=i+1,$ let $P_{2}=P_{1}.$
   Otherwise, $j>i+1,$ so components are added between $x_{i}$ and $x_{j}{\text{:}}$ add the components $x_{i+1},\dots ,x_{j-1}$ one by one using the tuple lemma's statement 2. This produces a class $P_{2}$ containing all the $j$-tuples $$(((\cdots ((x_{1},\dots ,x_{i}),x_{i+1}),\cdots ),x_{j-1}),x_{j})=(x_{1},\dots ,x_{j})$$ satisfying $R(x_{i},x_{j}).$
3. If $j=n,$ let $P_{3}=P_{2}.$
   Otherwise, $j<n,$ so components are added after $x_{j}{\text{:}}$ add the components $x_{j+1},\dots ,x_{n}$ one by one using the tuple lemma's statement 3. This produces a class $P_{3}$ containing all the $n$-tuples $$((\cdots ((x_{1},\dots ,x_{j}),x_{j+1}),\cdots ),x_{n})=(x_{1},\dots ,x_{n})$$ satisfying $R(x_{i},x_{j}).$
4. Let $Q=P_{3}\cap V^{n}.$ Extensionality implies that $Q$ is the unique class of $n$-tuples satisfying $R(x_{i},x_{j}).$

Class existence theorem for transformed formulas — Let $\phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})$ be a formula that:

1. contains no free variables other than $x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m}$;
2. contains only $\in$, $\neg$, $\land$, $\exists$, set variables, and the class variables $Y_{k}$ where $Y_{k}$ does not appear before an $\in$ ;
3. only quantifies set variables $x_{n+q}$ where $q$ is the quantifier nesting depth of the variable.

Then for all $Y_{1},\dots ,Y_{m}$, there exists a unique class $A$ of $n$-tuples such that: $$\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})].$$

Proof: Basis step: $\phi$ has 0 logical symbols. The theorem's hypothesis implies that $\phi$ is an atomic formula of the form $x_{i}\in x_{j}$ or $x_{i}\in Y_{k}.$

Case 1: If $\phi$ is $x_{i}\in x_{j}$, we build the class $E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\},$ the unique class of $n$-tuples satisfying $x_{i}\in x_{j}.$

Case a: $\phi$ is $x_{i}\in x_{j}$ where $i<j.$ The axiom of membership produces a class $P$ containing all the ordered pairs $(x_{i},x_{j})$ satisfying $x_{i}\in x_{j}.$ Apply the expansion lemma to $P$ to obtain $E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\}.$

Case b: $\phi$ is $x_{i}\in x_{j}$ where $i>j.$ The axiom of membership produces a class $P$ containing all the ordered pairs $(x_{i},x_{j})$ satisfying $x_{i}\in x_{j}.$ Apply the tuple lemma's statement 4 to $P$ to obtain $P'$ containing all the ordered pairs $(x_{j},x_{i})$ satisfying $x_{i}\in x_{j}.$ Apply the expansion lemma to $P'$ to obtain $E_{i,j,n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in x_{j}\}.$

Case c: $\phi$ is $x_{i}\in x_{j}$ where $i=j.$ Since this formula is false by the axiom of regularity, no $n$-tuples satisfy it, so $E_{i,j,n}=\emptyset .$

Case 2: If $\phi$ is $x_{i}\in Y_{k}$, we build the class $E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\},$ the unique class of $n$-tuples satisfying $x_{i}\in Y_{k}.$

Case a: $\phi$ is $x_{i}\in Y_{k}$ where $i<n.$ Apply the axiom of product by $V$ to $Y_{k}$ to produce the class $P=Y_{k}\times V=\{(x_{i},x_{i+1}):x_{i}\in Y_{k}\}.$ Apply the expansion lemma to $P$ to obtain $E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\}.$

Case b: $\phi$ is $x_{i}\in Y_{k}$ where $i=n>1.$ Apply the axiom of product by $V$ to $Y_{k}$ to produce the class $P=Y_{k}\times V=\{(x_{i},x_{i-1}):x_{i}\in Y_{k}\}.$ Apply the tuple lemma's statement 4 to $P$ to obtain $P'=V\times Y_{k}=\{(x_{i-1},x_{i}):x_{i}\in Y_{k}\}.$ Apply the expansion lemma to $P'$ to obtain $E_{i,Y_{k},n}=\{(x_{1},\ldots ,x_{n}):x_{i}\in Y_{k}\}.$

Case c: $\phi$ is $x_{i}\in Y_{k}$ where $i=n=1.$ Then $E_{i,Y_{k},n}=Y_{k}.$

Inductive step: $\phi$ has $k$ logical symbols where $k>0$. Assume the induction hypothesis that the theorem is true for all $\psi$ with less than $k$ logical symbols. We now prove the theorem for $\phi$ with $k$ logical symbols. In this proof, the list of class variables $Y_{1},\dots ,Y_{m}$ is abbreviated by ${\vec {Y}}$, so a formula—such as $\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})$—can be written as $\phi (x_{1},\dots ,x_{n},{\vec {Y}}).$

Case 1: $\phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\neg \psi (x_{1},\ldots ,x_{n},{\vec {Y}}).$ Since $\psi$ has $k-1$ logical symbols, the induction hypothesis implies that there is a unique class $A$ of $n$-tuples such that: $$\quad (x_{1},\ldots ,x_{n})\in A\iff \psi (x_{1},\ldots ,x_{n},{\vec {Y}}).$$ By the complement axiom, there is a class $\complement A$ such that $\forall u\,[u\in \complement A\iff \neg (u\in A)].$ However, $\complement A$ contains elements other than $n$-tuples if $n>1.$ To eliminate these elements, use $\complement _{V^{n}}A=\,$$\complement A\cap V^{n}=\,$$V^{n}\setminus A,$ which is the complement relative to the class $V^{n}$ of all $n$-tuples. Then, by extensionality, $\complement _{V^{n}}A$ is the unique class of $n$-tuples such that: $${\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in \complement _{V^{n}}A&&\iff \neg [(x_{1},\ldots ,x_{n})\in A]\\&&&\iff \neg \psi (x_{1},\ldots ,x_{n},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}$$

Case 2: $\phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}})\land \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}}).$ Since both $\psi _{1}$ and $\psi _{2}$ have less than $k$ logical symbols, the induction hypothesis implies that there are unique classes of $n$-tuples, $A_{1}$ and $A_{2}$, such that:

${\begin{aligned}\quad &(x_{1},\ldots ,x_{n})\in A_{1}\iff \psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}}).\\&(x_{1},\ldots ,x_{n})\in A_{2}\iff \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}}).\end{aligned}}$

By the axioms of intersection and extensionality, $A_{1}\cap A_{2}$ is the unique class of $n$-tuples such that: $${\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in A_{1}\cap A_{2}&&\iff (x_{1},\ldots ,x_{n})\in A_{1}\land (x_{1},\ldots ,x_{n})\in A_{2}\\&&&\iff \psi _{1}(x_{1},\ldots ,x_{n},{\vec {Y}})\land \psi _{2}(x_{1},\ldots ,x_{n},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}$$

Case 3: $\phi (x_{1},\ldots ,x_{n},{\vec {Y}})=\exists x_{n+1}\psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}}).$ The quantifier nesting depth of $\psi$ is one more than that of $\phi$ and the additional free variable is $x_{n+1}.$ Since $\psi$ has $k-1$ logical symbols, the induction hypothesis implies that there is a unique class $A$ of $(n+1)$-tuples such that: $$\quad (x_{1},\ldots ,x_{n},x_{n+1})\in A\iff \psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}}).$$ By the axioms of domain and extensionality, $Dom(A)$ is the unique class of $n$-tuples such that: $${\begin{alignedat}{2}\quad &(x_{1},\ldots ,x_{n})\in Dom(A)&&\iff \exists x_{n+1}[((x_{1},\ldots ,x_{n}),x_{n+1})\in A]\\&&&\iff \exists x_{n+1}[(x_{1},\ldots ,x_{n},x_{n+1})\in A]\\&&&\iff \exists x_{n+1}\,\psi (x_{1},\ldots ,x_{n},x_{n+1},{\vec {Y}})\\&&&\iff \phi (x_{1},\ldots ,x_{n},{\vec {Y}}).\end{alignedat}}$$

Gödel pointed out that the class existence theorem "is a metatheorem, that is, a theorem about the system [NBG], not in the system …" It is a theorem about NBG because it is proved in the metatheory by induction on NBG formulas. Also, its proof—instead of invoking finitely many NBG axioms—inductively describes how to use NBG axioms to construct a class satisfying a given formula. For every formula, this description can be turned into a constructive existence proof that is in NBG. Therefore, this metatheorem can generate the NBG proofs that replace uses of NBG's class existence theorem.

A recursive computer program succinctly captures the construction of a class from a given formula. The definition of this program does not depend on the proof of the class existence theorem. However, the proof is needed to prove that the class constructed by the program satisfies the given formula and is built using the axioms. This program is written in pseudocode that uses a Pascal-style case statement. $${\begin{array}{l}\mathbf {function} \;{\text{Class}}(\phi ,\,n)\\\quad {\begin{array}{rl}\mathbf {input} \!:\;\,&\phi {\text{ is a transformed formula of the form }}\phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m});\\&n{\text{ specifies that a class of }}n{\text{-tuples is returned.}}\\\;\;\;\;\mathbf {output} \!:\;\,&{\text{class }}A{\text{ of }}n{\text{-tuples satisfying }}\\&\,\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\ldots ,x_{n})\in A\iff \phi (x_{1},\ldots ,x_{n},Y_{1},\ldots ,Y_{m})].\end{array}}\\\mathbf {begin} \\\quad \mathbf {case} \;\phi \;\mathbf {of} \\\qquad {\begin{alignedat}{2}x_{i}\in x_{j}:\;\;&\mathbf {return} \;\,E_{i,j,n};&&{\text{// }}E_{i,j,n}\;\,=\{(x_{1},\dots ,x_{n}):x_{i}\in x_{j}\}\\x_{i}\in Y_{k}:\;\;&\mathbf {return} \;\,E_{i,Y_{k},n};&&{\text{// }}E_{i,Y_{k},n}=\{(x_{1},\dots ,x_{n}):x_{i}\in Y_{k}\}\\\neg \psi :\;\;&\mathbf {return} \;\,\complement _{V^{n}}{\text{Class}}(\psi ,\,n);&&{\text{// }}\complement _{V^{n}}{\text{Class}}(\psi ,\,n)=V^{n}\setminus {\text{Class}}(\psi ,\,n)\\\psi _{1}\land \psi _{2}:\;\;&\mathbf {return} \;\,{\text{Class}}(\psi _{1},\,n)\cap {\text{Class}}(\psi _{2},\,n);&&\\\;\;\;\;\,\exists x_{n+1}(\psi ):\;\;&\mathbf {return} \;\,Dom({\text{Class}}(\psi ,\,n+1));&&{\text{// }}x_{n+1}{\text{ is free in }}\psi ;{\text{ Class}}(\psi ,\,n+1)\\&\ &&{\text{// returns a class of }}(n+1){\text{-tuples}}\end{alignedat}}\\\quad \mathbf {end} \\\mathbf {end} \end{array}}$$

Let $\phi$ be the formula of example 2. The function call $A=Class(\phi ,1)$ generates the class $A,$ which is compared below with $\phi .$ This shows that the construction of the class $A$ mirrors the construction of its defining formula $\phi .$

$${\begin{alignedat}{2}&\phi \;&&=\;\;\exists x_{2}\,(x_{2}\!\in \!x_{1}\land \;\;\neg \;\;\;\;\exists x_{3}\;(x_{3}\!\in \!x_{2}))\,\land \;\;\,\exists x_{2}\,(x_{2}\!\in \!x_{1}\land \;\;\,\exists x_{3}\,(x_{3}\!\in \!x_{2}\,\land \;\;\neg \;\;\;\;\exists x_{4}\;(x_{4}\!\in \!x_{3})))\\&A\;&&=Dom\,(\;E_{2,1,2}\;\cap \;\complement _{V^{2}}\,Dom\,(\;E_{3,2,3}\;))\,\cap \,Dom\,(\;E_{2,1,2}\;\cap \,Dom\,(\;\,E_{3,2,3}\;\cap \;\complement _{V^{3}}\,Dom\,(\;E_{4,3,4}\;)))\end{alignedat}}$$

Расширение теоремы о существовании класса

Гёдель распространил теорему существования классов на формулы $\phi$ содержащие отношения над классами (например, $Y_{1}\subseteq Y_{2}$ и унарное отношение $M(Y_{1})$), специальные классы (такие как $Ord$ ) и операции (например, $(x_{1},x_{2})$ и $x_{1}\cap Y_{1}$). Чтобы расширить теорему о существовании классов, формулы, определяющие отношения, специальные классы и операции, должны давать количественную оценку только над множествами. Затем $\phi$ может быть преобразована в эквивалентную формулу, удовлетворяющую условию теоремы существования класса .

Следующие определения определяют, как формулы определяют отношения, специальные классы и операции:

1. Отношение $R$ определяется: $R(Z_{1},\dots ,Z_{k})\iff \psi _{R}(Z_{1},\dots ,Z_{k}).$
2. Специальный класс $C$ определяется: $u\in C\iff \psi _{C}(u).$
3. Операция $P$ определяется: $u\in P(Z_{1},\dots ,Z_{k})\iff \psi _{P}(u,Z_{1},\dots ,Z_{k}).$

Термин определяется :

1. Переменные и специальные классы являются терминами.
2. Если $P$ операция с $k$ аргументы и $\Gamma _{1},\dots ,\Gamma _{k}$ термины, тогда $P(\Gamma _{1},\dots ,\Gamma _{k})$ это термин.

Следующие правила преобразования устраняют отношения, специальные классы и операции. Каждый раз, когда правило 2b, 3b или 4 применяется к субформе, $i$ выбирается так, чтобы $z_{i}$ отличается от других переменных в текущей формуле. Правила повторяются до тех пор, пока не появятся субформлы, к которым они могут быть применены. $\,\Gamma _{1},\dots ,\Gamma _{k},\Gamma ,$ и $\Delta$ обозначают условия.

1. Отношение $R(Z_{1},\dots ,Z_{k})$ заменяется определяющей формулой $\psi _{R}(Z_{1},\dots ,Z_{k}).$
2. Позволять $\psi _{C}(u)$ быть определяющей формулой для специального класса $C.$
   1. $\Delta \in C$ заменяется на $\psi _{C}(\Delta ).$
   2. $C\in \Delta$ заменяется на $\exists z_{i}[z_{i}=C\land z_{i}\in \Delta ].$
3. Позволять $\psi _{P}(u,Z_{1},\dots ,Z_{k})$ быть определяющей формулой для операции $P(Z_{1},\dots ,Z_{k}).$
   1. $\Delta \in P(\Gamma _{1},\dots ,\Gamma _{k})$ заменяется на $\psi _{P}(\Delta ,\Gamma _{1},\dots ,\Gamma _{k}).$
   2. $P(\Gamma _{1},\dots ,\Gamma _{k})\in \Delta$ заменяется на $\exists z_{i}[z_{i}=P(\Gamma _{1},\dots ,\Gamma _{k})\land z_{i}\in \Delta ].$
4. Экстенсиональность используется для преобразования $\Delta =\Gamma$ в $\forall z_{i}(z_{i}\in \Delta \iff z_{i}\in \Gamma ).$

Пример 3:   Преобразование $Y_{1}\subseteq Y_{2}.$ $Y_{1}\subseteq Y_{2}\iff \forall z_{1}(z_{1}\in Y_{1}\implies z_{1}\in Y_{2})\quad {\text{(rule 1)}}$

Пример 4:   Преобразование $x_{1}\cap Y_{1}\in x_{2}.$ ${\begin{alignedat}{2}x_{1}\cap Y_{1}\in x_{2}&\iff \exists z_{1}[z_{1}=x_{1}\cap Y_{1}\,\land \,z_{1}\in x_{2}]&&{\text{(rule 3b)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\cap Y_{1})\,\land \,z_{1}\in x_{2}]&&{\text{(rule 4)}}\\&\iff \exists z_{1}[\forall z_{2}(z_{2}\in z_{1}\iff z_{2}\in x_{1}\land z_{2}\in Y_{1})\,\land \,z_{1}\in x_{2}]\quad &&{\text{(rule 3a)}}\\\end{alignedat}}$ Этот пример иллюстрирует, как правила преобразования работают вместе, чтобы исключить операцию.

Теорема существования класса (расширенная версия) — Пусть $\phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})$ быть формулой, которая количественно определяет только множества, не содержит никаких свободных переменных, кроме $x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m}$и может содержать отношения, специальные классы и операции, определяемые формулами, которые определяют количественно только над множествами. Тогда для всех $Y_{1},\dots ,Y_{m},$ существует уникальный класс $A$ из $n$-кортежи такие, что $$\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})].$$

Доказательство

Примените правила преобразования к $\phi$ для создания эквивалентной формулы, не содержащей отношений, специальных классов или операций. Эта формула удовлетворяет условию теоремы существования класса. Поэтому для всех $Y_{1},\dots ,Y_{m},$ есть уникальный класс $A$ из $n$- кортежи удовлетворяющие $$\forall x_{1}\cdots \,\forall x_{n}[(x_{1},\dots ,x_{n})\in A\iff \phi (x_{1},\dots ,x_{n},Y_{1},\dots ,Y_{m})].$$

Установите аксиомы

Аксиомы спаривания и регулярности, необходимые для доказательства теоремы существования классов, были приведены выше. NBG содержит еще четыре аксиомы набора. Три из этих аксиом относятся к операциям классов, применяемым к множествам.

Определение.   $F$ является функцией, если $$F\subseteq V^{2}\land \forall x\,\forall y\,\forall z\,[(x,y)\in F\,\land \,(x,z)\in F\implies y=z].$$

В теории множеств определение функции не требует указания области определения или кодомена функции (см. Функция (теория множеств) ). Определение функции NBG обобщает определение ZFC с набора упорядоченных пар на класс упорядоченных пар.

Определения ZFC операций над множествами image , Union и Power Set также обобщаются на операции классов. Образ класса $A$ под функцией $F$ является $F[A]=\{y:\exists x(x\in A\,\land \,(x,y)\in F)\}.$ Это определение не требует, чтобы $A\subseteq Dom(F).$ Союз класса $A$ является $\cup A=\{x:\exists y(x\in y\,\,\land \,y\in A)\}.$ Класс мощности $A$ является ${\mathcal {P}}(A)=\{x:x\subseteq A\}.$ Расширенная версия теоремы существования классов подразумевает существование этих классов. Аксиомы замены, объединения и степенного множества подразумевают, что когда эти операции применяются к множествам, они создают множества.

Аксиома замены.   Если $F$ это функция и $a$ это набор, то $F[a]$, образ ​ $a$ под $F$, представляет собой набор. $$\forall F\,\forall a\,[F{\text{ is a function}}\implies \exists b\,\forall y\,(y\in b\iff \exists x(x\in a\,\land \,(x,y)\in F))].$$

Не имея требования $A\subseteq Dom(F)$ в определении $F[A]$ дает более сильную аксиому замены, которая используется в следующем доказательстве.

NBG Теорема ( аксиома разделения ) — Если $a$ представляет собой набор и $B$ является подклассом $a,$ затем $B$ это набор.

Доказательство

Теорема существования класса строит ограничение тождественной функции на $B$: $I{\upharpoonright _{B}}=\{(x_{1},x_{2}):x_{1}\in B\land x_{2}=x_{1}\}.$ Поскольку образ $a$ под $I{\upharpoonright _{B}}$ является $B$, из аксиомы замены следует, что $B$ это набор. Это доказательство зависит от определения образа, не имеющего требования $a\subseteq Dom(F)$ с $Dom(I{\upharpoonright _{B}})=B\subseteq a$ скорее, чем $a\subseteq Dom(I{\upharpoonright _{B}}).$

Аксиома союза.   Если $a$ набор, тогда есть набор, содержащий $\cup a.$ $$\forall a\,\exists b\,\forall x\,[\,\exists y(x\in y\,\,\land \,y\in a)\implies x\in b\,].$$

Аксиома мощности.   Если $a$ набор, тогда есть набор, содержащий ${\mathcal {P}}(a).$

$\forall a\,\exists b\,\forall x\,(x\subseteq a\implies x\in b).$

Теорема - если $a$ это набор, то $\cup a$ и ${\mathcal {P}}(a)$ являются наборами.

Доказательство

Аксима Союза утверждает, что $\cup a$ это подкласс набора $b$, таким образом, аксиома разделения подразумевает $\cup a$ это набор. Аналогично, аксиома мощности утверждает, что ${\mathcal {P}}(a)$ это подкласс набора $b$, таким образом, аксиома разделения подразумевает, что ${\mathcal {P}}(a)$ это набор.

Аксиома бесконечности.   Существует неэпатный набор $a$ так что для всех $x$ в $a$, существует $y$ в $a$ так что $x$ является правильной подмножеством $y$. $$\exists a\,[\exists u(u\in a)\,\land \,\forall x(x\in a\implies \exists y(y\in a\,\land \,x\subset y))].$$

Аксиомы бесконечности и замены доказывают существование пустого набора . В обсуждении аксиомов существования класса существование пустого класса $\emptyset$ было доказано. Теперь мы докажем, что $\emptyset$ это набор. Пусть функция $F=\emptyset$ и пусть $a$ — множество, заданное аксиомой бесконечности. При замене изображение $a$ под $F$, что равно $\emptyset$, представляет собой набор.

Аксиома бесконечности NBG подразумевается аксиомой бесконечности ZFC : $\,\exists a\,[\emptyset \in a\,\land \,\forall x(x\in a\implies x\cup \{x\}\in a)].\,$ Первое соединение аксиомы ZFC, $\emptyset \in a$, подразумевает первое соединение аксиомы НБГ. Второе соединение аксиомы ZFC: $\forall x(x\in a\implies x\cup \{x\}\in a)$, подразумевает второе соединение аксиомы НБГ, поскольку $x\subset x\cup \{x\}.$ Чтобы доказать аксиому бесконечности ZFC на основе аксиомы бесконечности NBG, требуются некоторые другие аксиомы NBG (см. Слабая аксиома бесконечности ).

Аксиома глобального выбора

Концепция класса позволяет NBG иметь более сильную аксиому выбора, чем ZFC. Функция выбора - это функция $f$ определяется на сете $s$ непусты $f(x)\in x$ для всех $x\in s.$ Аксиома выбора ZFC гласит, что существует функция выбора для каждого набора непустых наборов. Функция глобального выбора - это функция $G$ определяется на классе всех непусты $G(x)\in x$ Для каждого непустого набора $x.$ Аксима глобального выбора гласит, что существует функция глобального выбора. Эта аксиома подразумевает аксиому ZFC, поскольку для каждого набора $s$ непустых наборов, $G\vert _{s}$ ( Ограничение ​ $G$ к $s$) является функцией выбора для $s.$ В 1964 году Уильям Б. Истон доказал, что глобальный выбор сильнее, чем аксиома выбора, используя принуждение к созданию модели , которая удовлетворяет аксиоме выбора и все аксиомы NBG, за исключением аксиомы глобального выбора. Аксиома глобального выбора эквивалентна каждому классу, имеющему хорошо упорядоченный, в то время как аксиома выбора ZFC эквивалентна каждому набору, имеющему хорошо упорядоченный.

Аксиома глобального выбора.   Существует функция, которая выбирает элемент из каждого непустых наборов.

$\exists G\,[G{\text{ is a function}}\,\land \forall x(x\neq \emptyset \implies \exists y(y\in x\land (x,y)\in G))].$

История

История подходов, которые привели к теории наборов NBG

Из системы аксиомы Неймана 1925 года

Фон Нейман опубликовал вступительную статью о своей системе аксиомы в 1925 году. В 1928 году он предоставил подробную обработку своей системы. Фон Нейман основал свою систему аксиомы на двух доменах примитивных объектов: функции и аргументы. Эти домены перекрываются-объекты, которые находятся в обеих областях, называются функциями аргументов. Функции соответствуют классам в NBG, а функции аргументов соответствуют наборам. Примитивной операцией фон Неймана является применение функции , обозначаемое [ a , x ], а не ( ) x , где a является функцией, а X - аргумент. Эта операция создает аргумент. Фон Нейман определял классы и наборы, используя функции и функции аргументов, которые занимают только два значения A и B. , Он определил x ∈ A, если [ a , x ] ↓ a .

На работу фон Неймана в теории наборов были повлияли Георга Кантора статьи , аксиомы Эрнста Зермело в 1908 году для теории наборов и критические виды Авраама теории наборов Zermelo, которые были даны независимо от Фрэенкеля и Торалфа Сколем . аксиомы Зермело не могут доказать существование набора { z ₀ , z ₁ , z ₂ , ...}, где z ₀ - набор натуральных чисел , а z _{n +1} - набор мощности z И Фраенкель, и Сколем отметили, что _не ​Затем они ввели аксиому замены, которая гарантирует существование таких наборов. Однако они не хотели принимать эту аксиому: Френкель заявил, что «Замена была слишком сильной аксиомой для «общей теории множеств»», в то время как «Скулем только писал, что« мы могли бы ввести Замену ».

Фон Нейман работал над проблемами теории множеств Цермело и предложил решения некоторых из них:

• Теория ординалов
  • Кантора Проблема: теория порядковых чисел не может быть развита в теории множеств Цермело, поскольку в ней отсутствует аксиома замены.
  • Решение: Фон Нейман восстановил теорию Кантора, определив ординалы с использованием множеств, которые хорошо упорядочены с помощью отношения £: и, используя аксиому замены, чтобы доказать ключевые теоремы о ординалах, таких как каждый хорошо упорядоченный набор, является порядок изоморфного с порядком. В отличие от Фраенкеля и Сколема, фон Нейман, подчеркнул, насколько важна аксиома замены для теории наборов: «Фактически, я считаю, что никакая теория ординалов вообще невозможна без этой аксиомы».
• Критерий, определяющий классы, которые слишком велики, чтобы быть наборами
  • Проблема: Zermelo не дал такого критерия. Его теория наборов позволяет избежать больших классов, которые ведут к парадоксам , но она оставляет много наборов, таких как тот, который упоминается Фрэнкель и Сколем.
  • Решение: фон Нейман ввел критерий: класс слишком велик, чтобы быть набором, если и только тогда, когда его можно отобрать на класс V всех наборов. Фон Нейман понял, что теоретичные парадоксы можно избежать, не позволяя таким большим классам быть членами какого-либо класса. Сочетая это ограничение с его критерием, он получил свою аксиому ограничения размера : класс C не является членом какого -либо класса, если и только если может быть отображен на V. C
• Конечная аксиоматизация
  • Проблема: Zermelo использовал неточную концепцию «определенной пропозициональной функции » в своей аксиоме разделения .
  • Решения: Скулем представил аксиоматическую схему разделения , которая позже использовалась в ZFC, а Френкель предложил эквивалентное решение. Однако Цермело отверг оба подхода, «особенно потому, что они неявно включают концепцию натурального числа, которая, по мнению Цермело, должна основываться на теории множеств». Фон Нейман избегал схем аксиом , формализуя понятие «определенной пропозициональной функции» с помощью своих функций, для построения которых требуется только конечное число аксиом. Это привело к тому, что его теория множеств имела конечное число аксиом. В 1961 году Ричард Монтегю доказал, что ZFC не может быть конечно аксиоматизирован.
• Аксиома регулярности
  • Проблема: теория множеств Цермело начинается с пустого множества и бесконечного множества и повторяет аксиомы спаривания, объединения, степенного множества, разделения и выбора для создания новых множеств. Однако это не ограничивает наборы только ими. Например, он допускает наборы, которые не являются обоснованными , например набор x, удовлетворяющий x ∈ x .
  • Решения: Френкель ввел аксиому, исключающую эти множества. Фон Нейман проанализировал аксиому Френкеля и заявил, что она не была «точно сформулирована», но приблизительно говорила бы: «Помимо множеств... существование которых абсолютно требуется аксиомами, других множеств не существует». Фон Нейман предложил аксиому регулярности как способ исключения необоснованных множеств, но не включил ее в свою систему аксиом. В 1930 году Цермело первым опубликовал систему аксиом, включающую регулярность.

Система аксиом фон Неймана 1929 года

Джон фон Нейман

В 1929 году фон Нейман опубликовал статью, содержащую аксиомы, которые привели бы к NBG. Эта статья была мотивирована его беспокойством по поводу непротиворечивости аксиомы ограничения размера. Он заявил, что эта аксиома «делает очень многое, даже слишком многое». Помимо применения аксиом разделения и замены и теоремы о хорошем порядке , из этого также следует, что любой класс, мощность которого меньше мощности V, является множеством. Фон Нейман подумал, что этот последний вывод выходит за рамки канторианской теории множеств, и пришел к выводу: «Поэтому мы должны обсудить, не является ли ее [аксиома] последовательность даже более проблематичной, чем аксиоматизация теории множеств, которая не выходит за рамки необходимой канторианской структуры».

Фон Нейман начал свое исследование непротиворечивости с введения своей системы аксиом 1929 года, которая содержит все аксиомы его системы аксиом 1925 года, за исключением аксиомы ограничения размера. Он заменил эту аксиому двумя ее следствиями: аксиомой замены и аксиомой выбора. Аксиома выбора фон Неймана гласит: «Каждое отношение R имеет подкласс, который является функцией с той же областью определения, что и R ».

Пусть S — система аксиом фон Неймана 1929 года. Фон Нейман ввел систему аксиом S + Регулярность (которая состоит из S и аксиомы регулярности), чтобы продемонстрировать, что его система 1925 года непротиворечива относительно S . Он доказал:

1. Если S согласован, то S + регулярность согласована.
2. S + Регулярность подразумевает аксиому ограничения размера. Поскольку это единственная аксиома его системы аксиомы 1925 года, которой S не имеет регулярности +, S + регулярность подразумевает все аксиомы его системы 1925 года.

Эти результаты подразумевают: если S согласован, то система аксиомы фон Неймана 1925 года согласована. Доказательство: если S согласован, то S + регулярность является последовательной (результат 1). Используя доказательство по противоречию , предположим, что система аксиомы 1925 года не соответствует или эквивалентно: система аксиомы 1925 года подразумевает противоречие. Поскольку S + регулярность подразумевает аксиомы системы 1925 года (результат 2), S + регулярность также подразумевает противоречие. Тем не менее, это противоречит согласованности регулярности S +. Следовательно, если S согласован, то система аксиомы фон Неймана 1925 года согласована.

Поскольку S — это его система аксиом 1929 года, система аксиом фон Неймана 1925 года непротиворечива по отношению к его системе аксиом 1929 года, которая ближе к канторианской теории множеств. Основными различиями между канторианской теорией множеств и системой аксиом 1929 года являются классы и аксиома выбора фон Неймана. Система аксиом S + Regularity была модифицирована Бернейсом и Гёделем для создания эквивалентной системы аксиом NBG.

Система аксиом Бернейса

Пол Бернайс

В 1929 году Пауль Бернейс начал модифицировать новую систему аксиом фон Неймана, взяв классы и множества в качестве примитивов. Он опубликовал свою работу в серии статей, выходивших с 1937 по 1954 год. Бернейс заявил, что:

Цель модификации системы фон Неймана состоит в том, чтобы оставаться ближе к структуре исходной системы Zermelo и в то же время использовать некоторые из теоретичных концепций логики Schröder и основной математики, которые стали знакомыми логикам. Как будет видно, значительные результаты упрощения из этого соглашения.

Бернайс обрабатывал наборы и классы в двух сортированной логике и представил два примитива членства: один для членства в наборах и один для членства в классах. С этими примитивами он переписал и упростил аксиомы фон Неймана 1929 года. Бернайс также включал аксиому регулярности в его системе аксиомы.

Система аксиом Гёделя (NBG)

Курт Гёдель,      ок. 1926 год

В 1931 году Бернейс отправил письмо, содержащее свою теорию множеств, Курту Гёделю . Гёдель упростил теорию Бернейса, сделав каждое множество классом, что позволило ему использовать только один вид и один примитив членства. Он также ослабил некоторые аксиомы Бернейса и заменил аксиому выбора фон Неймана эквивалентной аксиомой глобального выбора. Гёдель использовал свои аксиомы в своей монографии 1940 года об относительной последовательности глобального выбора и гипотезе обобщенного континуума.

Было приведено несколько причин для выбора NBG для его монографии:

• Гедель дал математическую причину - глобальный выбор NBG дает более сильную теорему последовательности: «Эта более сильная форма аксиомы [выбора], если согласуется с другими аксиомами, конечно, что более слабая форма также является последовательной».
• Роберт Соловай предположил: «Я предполагаю, что он [Гёдель] хотел избежать обсуждения технических особенностей, связанных с разработкой зачатий теории модели в теории аксиоматических наборов».
• Кеннет Кунен объяснил, почему Гёдель избегает этой дискуссии: «Существует также гораздо более комбинаторный подход к L [ конструируемой вселенной ], разработанный… [Гёделем в его монографии 1940 года] в попытке объяснить свою работу не- логики... Достоинство этого подхода состоит в том, что он удаляет все остатки логики из трактовки L ».
• Чарльз Парсонс обосновал философское обоснование выбора Гёделя: «Эта точка зрения [что «свойство множества» является примитивом теории множеств] может быть отражено в выборе Гёделем теории с переменными класса в качестве основы для… [его монографии] ."

Достижения Гёделя вместе с деталями его презентации привели к известности, которой NBG будет пользоваться в течение следующих двух десятилетий. В 1963 году Пол Коэн доказал свои доказательства независимости для ZF с помощью некоторых инструментов, которые Гёдель разработал для своих доказательств относительной непротиворечивости для NBG. Позже ZFC стал популярнее NBG. Это было вызвано несколькими факторами, включая дополнительную работу, необходимую для обработки выгонки в НБГ, Презентация Коэна о принуждении 1966 года, в которой использовался ZF, и доказательство того, что NBG является консервативным расширением ZFC.

NBG, ZFC и MK

NBG не логически эквивалентен ZFC, потому что его язык более выразительен: он может делать утверждения о классах, которые не могут быть сделаны в ZFC. Тем не менее, NBG и ZFC подразумевают те же утверждения о наборах. Следовательно, NBG является консервативным расширением ZFC. NBG подразумевает теоремы, которые ZFC не подразумевает, но, поскольку NBG является консервативным расширением, эти теоремы должны включать надлежащие классы. Например, это теорема NBG, что глобальная аксиома выбора подразумевает, что надлежащий класс может быть хорошо упорядочен и что каждый правильный класс может быть помещен в одно-одному-соответствие с V. V

Одним из последствий консервативного расширения является то, что ZFC и NBG эквисогласованы . Для доказательства этого используется принцип взрыва : из противоречия все доказуемо. Предположим, что ZFC или NBG несовместимы. Тогда из противоречивой теории вытекают противоречивые утверждения ∅ = ∅ и ∅ ≠ ∅, которые являются утверждениями о множествах. В силу свойства консервативного расширения другая теория также подразумевает эти утверждения. Следовательно, это также противоречиво. Таким образом, хотя NBG более выразителен, он в равной степени соответствует ZFC. Этот результат вместе с доказательством относительной непротиворечивости фон Неймана 1929 года подразумевает, что его система аксиом 1925 года с аксиомой ограничения размера эквисовместима с ZFC. Это полностью снимает беспокойство фон Неймана по поводу относительной непротиворечивости этой мощной аксиомы, поскольку ZFC находится в рамках канторианской структуры.

Несмотря на то, что NBG является консервативным расширением ZFC, теорема может иметь более короткое и элегантное доказательство в NBG, чем в ZFC (или наоборот). Обзор известных результатов такого рода см. в Pudlák 1998 .

Теория множеств Морса – Келли имеет схему аксиом понимания классов, которая включает формулы, кванторы которых варьируются по классам. МК является более сильной теорией, чем НБГ, поскольку МК доказывает непротиворечивость НБГ. в то время как вторая теорема Гёделя о неполноте подразумевает, что NBG не может доказать непротиворечивость NBG.

Обсуждение некоторых онтологических и других философских проблем, поставленных NBG, особенно в сравнении с ZFC и MK, см. в Приложении C к Potter 2004 .

Модели

ZFC, NBG и MK имеют модели , описываемые в терминах кумулятивной иерархии V _α   и конструктивной иерархии L _α   . Пусть V включает недоступный кардинал κ, пусть ⊆ V κ _и пусть Def( X ) обозначает класс первого порядка определимых подмножеств X X с параметрами. В символах, где " $(X,\in )$" обозначает модель с доменом $X$ и отношение $\in$, и " $\models$«обозначает отношение удовлетворения : $$\operatorname {Def} (X):={\Bigl \{}\{x\mid x\in X{\text{ and }}(X,\in )\models \phi (x,y_{1},\ldots ,y_{n})\}:\phi {\text{ is a first-order formula and }}y_{1},\ldots ,y_{n}\in X{\Bigr \}}.$$

Затем:

• $(V_{\kappa },\in )$ и $(L_{\kappa },\in )$ являются моделями ZFC .
• ( V _κ , V _κ+1 , ∈) — модель МК, где V _κ состоит из множеств модели, а V _κ+1 состоит из классов модели. Поскольку модель МК является моделью НБГ, эта модель также является моделью НБГ.
• ( V _κ , Def( V _κ ), ∈) — это модель версии NBG Мендельсона, которая заменяет аксиому глобального выбора NBG аксиомой выбора ZFC. Аксиомы ZFC верны в этой модели, потому что ( V _κ , ∈) является моделью ZFC. В частности, аксиома выбора ZFC верна, но глобальный выбор NBG может потерпеть неудачу. Аксиомы существования классов NBG верны в этой модели, поскольку классы, существование которых они утверждают, могут быть определены определениями первого порядка. Например, аксиома принадлежности справедлива, поскольку класс $E$ определяется: $$E=\{x\in V_{\kappa }:(V_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.$$
• ( L _κ , L _{κ ⁺} , ∈), где κ ⁺ является кардиналом-преемником κ, является моделью NBG. Аксиомы существования классов NBG верны в ( L _κ , L _{κ ⁺} , ∈). Например, аксиома членства удерживается после класса $E$ определяется: $$E=\{x\in L_{\kappa }:(L_{\kappa },\in )\models \exists u\ \exists v[x=(u,v)\land u\in v]\}.$$ Таким образом, e ∈ 𝒫 ( L _κ ). В своем доказательстве, что GCH верно в L , Гёдель доказал, что 𝒫 ( L _κ ) ⊆ L _{κ ⁺} . Следовательно, e ∈ L _{κ ⁺} , таким образом, аксиома членства верна ( L _κ , L _{κ ⁺} , ∈). Аналогично, другие аксиомы существования в классе верны. Аксиома глобального выбора верна, потому что L _κ хорошо упорядочена ограничением функции ( Гёделя которая отображает класс ординалов для конструктивных наборов) до ординалов меньше, чем κ. Следовательно, ( L _κ , L _{κ ⁺} ∈) является моделью NBG.
• Если $M$ это нестандартная модель $\mathrm {ZFC}$, затем $(M,\mathrm {Def} (M))\vDash \mathrm {GB} +\Delta _{1}^{1}{\text{-CA}}$ эквивалентен «существует $X$ так что $(M,X)\vDash \mathrm {GB} +\Delta _{1}^{1}{\text{-CA}}$", где $\mathrm {Def} (M)$ это набор подмножеств $M$ которые определены над $M$. Это обеспечивает часть второго порядка для расширения данной нестандартной модели первого порядка $\mathrm {ZFC}$ к нестандартной модели $\mathrm {GB}$, если есть такое расширение вообще.

Теория категории

Онтология NBG обеспечивает леса для разговора о «больших объектах» без риска парадокса. Например, в некоторых событиях теории категории « большая категория » определяется как тот, чьи объекты и морфизмы составляют правильный класс. С другой стороны, «маленькая категория» - это та, чьи объекты и морфизмы являются членами набора. Таким образом, мы можем говорить о « категории всех наборов » или « категории всех небольших категорий » без риска парадокса, поскольку NBG поддерживает большие категории.

Тем не менее, NBG не поддерживает «категорию всех категорий», поскольку крупные категории будут его членами, а NBG не позволяет надлежащим классам быть членами чего -либо. Онтологическое расширение, которое позволяет нам официально говорить о такой «категории», - это конгломерат , который представляет собой набор классов. Тогда «категория всех категорий» определяется его объектами: конгломератом всех категорий; и его морфизмы: конгломерат всех морфизмов от A до B , где A и B являются объектами. О том, является ли онтология, включая классы, а также наборы адекватны для теории категорий, см. Muller 2001 .

Библиография

• Адамек, Иржи; Херрлих, Хорст; Стрекер, Джордж Э. (1990), Абстрактные и конкретные категории (Радость кошек) (1-е изд.), Нью-Йорк: Wiley & Sons, ISBN  978-0-471-60922-3 .
  • Адамек, Иржи; Херрлих, Хорст; Стрекер, Джордж Э. (2004) [1990], Абстрактные и конкретные категории (Радость кошек) (изд. Дувра), Нью-Йорк: Dover Publications, ISBN  978-0-486-46934-8 .
• Бернейс, Пол (1937), «Система аксиоматической теории множеств — Часть I», Журнал символической логики , 2 (1): 65–77, doi : 10.2307/2268862 , JSTOR   2268862 .
• Бернейс, Пол (1941), «Система аксиоматической теории множеств — Часть II», Журнал символической логики , 6 (1): 1–17, doi : 10.2307/2267281 , JSTOR   2267281 , S2CID   250344277 .
• Бернейс, Пол (1991), Аксиоматическая теория множеств (2-е исправленное издание), Dover Publications, ISBN  978-0-486-66637-2 .
• Бурбаки, Николя (2004), Элементы математики: теория множеств , Springer, ISBN  978-3-540-22525-6 .
• Чуаки, Роландо (1981), Аксиоматическая теория множеств: импредикативные теории классов , Северная Голландия, ISBN  0-444-86178-5 .
• Коэн, Пол (1963), «Независимость гипотезы континуума», Proceedings of the National Academy of Sciences of the United States of America , 50 (6): 1143–1148, Bibcode : 1963PNAS...50.1143C , doi : 10.1073/пнас.50.6.1143 , ПМЦ   221287 , ПМИД   16578557 .
• Коэн, Пол (1966), Теория множеств и гипотеза континуума , В.А. Бенджамин .
  • Коэн, Пол (2008), Теория множеств и гипотеза континуума , Dover Publications, ISBN  978-0-486-46921-8 .
• Доусон, Джон В. (1997), Логические дилеммы: жизнь и творчество Курта Гёделя , Уэлсли, Массачусетс: AK Peters .
• Истон, Уильям Б. (1964), Полномочия обычных кардиналов (докторская диссертация), Принстонский университет .
• Фельгнер, Ульрих (1971), «Сравнение аксиом локального и универсального выбора» (PDF) , Fundamenta Mathematicae , 71 : 43–62, doi : 10.4064/fm-71-1-43-62 .
• Феррейрос, Хосе (2007), Лабиринт мысли: история теории множеств и ее роль в математической мысли (2-е исправленное издание), Базель, Швейцария: Birkhäuser, ISBN  978-3-7643-8349-7 .
• Гёдель, Курт (1940), Согласованность аксиомы выбора и обобщенной гипотезы континуума с аксиомами теории множеств (пересмотренная редакция), Princeton University Press, ISBN  978-0-691-07927-1 .
  • Гёдель, Курт (2008), Согласованность аксиомы выбора и обобщенной гипотезы континуума с аксиомами теории множеств , с предисловием Лейвера, Ричарда (изд. в мягкой обложке), Ishi Press, ISBN  978-0-923891-53-4 .
• Гёдель, Курт (1986), Собрание сочинений, Том 1: Публикации 1929–1936 , Oxford University Press, ISBN  978-0-19-514720-9 .
• Гёдель, Курт (1990), Собрание сочинений, Том 2: Публикации 1938–1974 , Oxford University Press, ISBN  978-0-19-514721-6 .
• Гёдель, Курт (2003), Собрание сочинений, Том 4: Переписка A – G , Oxford University Press, ISBN  978-0-19-850073-5 .
• Грей, Роберт (1991), «Компьютерные программы и математические доказательства», The Mathematical Intelligencer , 13 (4): 45–48, doi : 10.1007/BF03028342 , S2CID   121229549 .
• Халлетт, Майкл (1984), Канторианская теория множеств и ограничение размера (изд. в твердом переплете), Оксфорд: Clarendon Press, ISBN  978-0-19-853179-1 .
  • Халлетт, Майкл (1986), Канторианская теория множеств и ограничение размера (изд. в мягкой обложке), Оксфорд: Clarendon Press, ISBN  978-0-19-853283-5 .
• Канамори, Акихиро (2009b), Высшая бесконечность: большие кардиналы в теории множеств с самого начала , Springer, ISBN  978-3-540-88867-3 .
• Канамори, Акихиро (2009), «Бернейс и теория множеств» (PDF) , Бюллетень символической логики , 15 (1): 43–69, doi : 10.2178/bsl/1231081769 , JSTOR   25470304 , CID   2562 45 .
• Kanamori, Akihiro (2012), «В похвале замене» (PDF) , Бюллетень символической логики , 18 (1): 46–90, doi : 10.2178/bsl/1327328439 , jstor   41472440 , s2cid   18951854 .
• Kunen, Kenneth (1980), Теория набора: введение в доказательства независимости (изд.), Северная Голландия, ISBN  978-0-444-86839-8 .
  • Kunen, Kenneth (2012), Теория набора: введение в доказательства независимости (в мягкой обложке изд.), Северная Голландия, ISBN  978-0-444-56402-3 .
• Mendelson, Elliott (1997), Введение в математическую логику (4 -е изд.), Лондон: Чепмен и Холл/CRC, ISBN  978-0-412-80830-2 Полем - стр. 225–86 содержит классическую учебную обработку NBG, показывая, как он делает то, что мы ожидаем от теории наборов, замывая отношения , теорию порядка , порядковые числа , трансфинитные числа и т. Д.
• Мириманофф, Дмитрий (1917), «Антиномии Рассела и Бури-Форти и фундаментальная проблема наборов наборов», Математическое образование , 19 : 37–52 .
• Montague, Richard (1961), «Семантическое закрытие и нефинансированная аксиоматизируемость I», в Buss, Сэмюэль Р. (ред.), Неосказания: Материалы симпозиума на основаниях математики , Pergamon Press, с. 45–69 .
• Мостовский, Анджей (1950), «Некоторые непредикативные определения в аксиоматической теории множеств» (PDF) , Fundamenta Mathematicae , 37 : 111–124, doi : 10.4064/fm-37-1-111-124 .
• Мюллер, Ф.А. (1 сентября 2001 г.), «Множества, классы и категории» (PDF) , Британский журнал философии науки , 52 (3): 539–73, doi : 10.1093/bjps/52.3.539 .
• Мюллер, Гурт, изд. (1976), Множества и классы: о работах Пола Бернейса , Исследования по логике и основам математики, том 84, Амстердам: Северная Голландия, ISBN  978-0-7204-2284-9 .
• Поттер, Майкл (2004), Теория набора и ее философия: критическое введение (жесткий переплет изд.), Oxford University Press, ISBN  978-0-19-926973-0 .
  • Поттер, Майкл (2004p), Теория сет и ее философия: критическое введение (в мягкой обложке изд.), Oxford University Press, ISBN  978-0-19-927041-5 .
• Pudlák, Pavel (1998), «Длина доказательств» (PDF) , в Buss, Samuel R. (ed.), Справочник по теории доказательств , Elsevier, с. 547–637, ISBN  978-0-444-89840-1 .
• Смуллян, Рэймонд . Fitting, Melvin (2010) [Пересмотренное и исправленное издание: впервые опубликовано в 1996 году издательством Oxford University Press], «Теория установок» и «Проблема континуума» , Dover, ISBN  978-0-486-47484-7 .
• Соловей, Роберт М. (1990), «Вступительная записка к 1938 , 1939 , 1939a и 1940 годам », Собрание сочинений Курта Гёделя, том 2: публикации 1938–1974 годов , Oxford University Press, стр. 1–25, ISBN  978-0-19-514721-6 .
• фон Нейман, Джон (1923), «О введении трансфинитных чисел» , Acta Litt. акад. наук. Сегед X. , 1 : 199–208 .
  • Английский перевод: ван Хейеноорт, Жан (2002a) [1967], «О введении трансфинитных чисел» , От Фреге до Гёделя: Справочник по математической логике, 1879–1931 (четвертое издание), Harvard University Press, стр. 346– 354, ISBN  978-0-674-32449-7 .
  • Английский перевод: Van Heijenoort, Jean (2002b) [1967], «Аксиоматизация теории наборов» , от Frege до Gödel: исходная книга по математической логике, 1879-1931 (Четвертая печать изд.) , ISBN  978-0-674-32449-7 .
• фон Нейман, Джон (1925), «Аксиоматизация теории множеств» , Журнал чистой и прикладной математики , 154 : 219–240 .
• Фон Нейман, Джон (1928), «Аксиоматизация величин» , Математический журнал , 27 : 669–752, doi : 10.1007/bf01171122 , s2cid   123492324 .
• фон Нейман, Джон (1929), «О свободе противоречия в аксиоматическом количестве преподавания» , журнал для чистой и прикладной математики , 160 : 227–241 .

Внешние ссылки

• «Фон Нейман-Бернейс-Гёдель теория» . Planetmath .
• Шудзик, Мэтью. «Фон Нейман-Бернейс-Гёдель теория» . MathWorld .