Las otras respuestas han explicado que estos esquemas de axioma de ZFC tiene que ser esquemas y no los axiomas, porque queremos que ZFC a ser de primer orden de la teoría. El razonamiento es que necesitamos cuantificar sobre todas las fórmulas de más de ZFC. En particular, la Especificación del esquema de ZFC puede ser enunciada como:
Para cada una de las $(k+1)$-parámetro de la sentencia de $φ$, ZFC tiene el axioma:
$∀p[1..k]\ ∀A\ ∃B\ ∀x\ ( x∈B ⇔ x∈A ∧ φ(p[1..k],x) )$.
Aviso que no podemos tener un solo axioma de que cuantifica sobre todos los parametrizadas frases (sobre la teoría en sí misma), debido a que no es (directamente) que se puede expresar en la lógica de primer orden. De hecho, se puede demostrar que ZFC no puede ser finitely axiomatized (utilizando el mismo lenguaje).
Pero eso no es bastante la historia completa. En general, existe un procedimiento para convertir cualquier suficientemente agradable de primer orden de la teoría de la $T$ a otro de primer orden de la teoría de la $T'$ (con un idioma diferente) que interpreta a $T$ y, sin embargo, es finitely axiomatized. Haciendo esto PA los rendimientos de un conocido de segundo orden llamada teoría ACA0, y haciendo esto para ZFC produce casi NBG.
La idea básica para el uso de dos tipos, una especie $I$ para el dominio original de $T$, y el otro tipo $J$ 'clases', donde cada clase es de una subcolección de $I$ que representa a algunos de predicado más de $T$. (Para ello, necesitamos $T$ a de apoyo razonable ordenó par de codificación.) Luego nos axiomatize la existencia de la clase de todos los objetos en $I$, es decir, $∃C∈J\ ∀x∈I\ ( x∈C )$, que para su comodidad hemos de estado como la existencia de la clase $\{ x : x∈I \}$. También axiomatize la existencia de la clase $\{ (x,x) : x∈I \}$ a la captura de la igualdad, y la existencia de una clase para la captura de cada predicado/función-símbolo de $T$. Por ejemplo, para capturar a "$∈$" de ZFC tendríamos la clase $\{ (x,y) : x,y∈I ∧ x∈y \}$. También axiomatize existencia de la clase singleton $\{x\}$ cualquier $x∈I$, y que las clases son cerrados bajo complemento, unión, intersección, producto cartesiano y la proyección.
Si $T$ tenía un número finito de predicado/símbolos de función, los axiomas son un número finito, y, sin embargo, nos permiten construir cualquier definibles clase de tuplas más de $T$, es decir, $\{ x[1..k] : φ(x[1..k]) \}$ cualquier $k$-parámetro de la sentencia de $φ$ sobre $T$, como miembro de la $J$. Además, cada clase que podemos construir explícitamente corresponde a algunos parametrizadas sentencia de más de $T$. Por lo tanto ahora podemos expresar cualquier axioma esquema de $T$ que cuantifica sobre todos los parametrización a penas de más de $T$ como un único axioma sobre la cuantificación de todos los miembros de $J$, y se puede demostrar que el resultado de la teoría de la $T'$ es conservador más de $T$ en el específico sentido de que cada frase de más de $T$ es comprobable por $T$ iff su traducción (es decir, la restricción de cada cuantificador a $I$) es comprobable por $T'$.
Desde muchos ordenados de primer orden de la teoría puede ser fácilmente interpretado por una ordenados de primer orden de la teoría (es decir, la sustitución de la clase por el predicado-símbolos), es intrascendente que hemos utilizado dos tipos de $T'$.
Muy aparte de lo finito axiomatizability de NBG, algunos teóricos prefieren decir que están trabajando en NBG en lugar de ZFC, ya que intrínsecamente permite la definición y cuantificación de las clases. Pero si uno quiere ser capaz de definir una clase cuya definición fórmula consiste en la cuantificación de las clases (como uno puede, en ZFC definir un conjunto cuya definición fórmula puede cuantificar sobre los conjuntos), entonces el resultado (MK) es de nuevo ya no finitely axiomatizable (en el idioma de NBG), debido a que se necesita un axioma esquema para la Especificación de las clases.
