Edward Nelson explicó muy bien en el Capítulo 2 de un papel que solía ser en su página de inicio en la universidad de Princeton ("quitado de revisión" hace varios años). Voy a tratar de hacer lo mismo utilizando mi comprensión adquirida a partir de él, ya que no se puede señalar que el papel nada más. En lógica se muestra (extensión por contigüidad de un símbolo de función) que si φ es una fórmula cuyas variables libres se x,x1,…,xn, y si ∀x1…∀xn∃xφ es un teorema, entonces podemos lindan con un nuevo n-ary símbolo de función f y el axioma ∀x1…∀xn[fx1…xn/x]φ para obtener un conservador de extensión. Pero un conservador de extensión si se aplica a la teoría de conjuntos no contiene nuevo conjunto de axiomas de la teoría de permitir que el nuevo símbolo de función que aparecen en los axiomas obtenidos a partir de la separación (subconjunto) y reemplazo (o colección) de esquema. En la práctica, esto no hace ninguna diferencia si la extensión es lo que se llama una extensión, por definición, lo cual ocurre cuando la declaración más fuerte en la ∀x1…∀xn∃!xφ sostiene (donde ∃!x significa que "no existe un único x tal que"). La razón es que en este caso, cualquier fórmula que contiene f puede ser traducido a un equivalente (en extensión) que la fórmula no contiene f, que la fórmula está permitido en la separación y reemplazo de los axiomas. También, cuando se φ no contiene variables libres distinta de x no hay ningún problema con lo que permite a la (constante especial, 0-ary) f a aparecer en la sustitución y la separación de los axiomas, ya que esos axiomas se mantenga al f es reemplazado por una variable que no aparece en los axiomas (y la sustitución tiene).
Del mismo modo, si ψ es una fórmula con variables libres x1,…,xn, podemos lindan con un nuevo n-ary predicado símbolo p, junto con la definición de axioma ∀x1…∀xn(px1…xn↔ψ). Estos también son llamados extensiones, por definición, presumiblemente debido a las declaraciones que implican p son traducibles a equivalente declaraciones no implican p. Ser traducible, de nuevo hay ningún problema permitiendo a los nuevos símbolos de predicado derivadas de las extensiones mediante la definición de un predicado símbolo aparezca en la separación y reemplazo de los axiomas.
En la práctica, haciendo que la teoría de conjuntos o de la matemática superior, basado en la teoría de conjuntos, uno puede utilizar las extensiones, por definición, y extensiones de constantes especiales con abandono, incluso en la separación y reemplazo de los axiomas. De hecho, las matemáticas sería impractically tedioso, a menos que este o algo similar. Pero cuando uno utiliza las extensiones por contigüidad de un símbolo de función que no son extensiones de la definición de un símbolo de función, como sucede cuando la singularidad de condición de falla, uno necesita algo como el axioma de elección para reformular los símbolos de función, de modo que puede ser utilizado en la separación y reemplazo de los axiomas. En la práctica, lo que esto significa es que cualquier función de los símbolos debe corresponder a las funciones obtenible por el axioma de elección. A menudo (por ejemplo, cuando las variables rango de más de conjuntos como el conjunto de los números reales) el axioma de elección puede ser utilizado para reemplazar algo como ∀x1…∀xn∃xφ con algo como ∃f∀x1…∀xn[f(x1,…,xn)/x]φ, donde aquí f es una variable que representa un conjunto teórico de la función y el paréntesis denotan un símbolo de función definición de evaluación (para cada función y argumento corresponde una única evaluación de la función en ese argumento, y por lo que la evaluación puede ser definida problemas-libre, por extensión, por definición de la función de símbolo). La declaración de ∃f∀x1…∀xn[f(x1,…,xn)/x]φ puede ser utilizado para lindan con un símbolo de función fc correspondiente a f que no causan los problemas que aparecen en la separación o el reemplazo de los axiomas siempre φ sólo involucra x,x1,…,xn como variables libres, porque entonces fc podría ser definido como una constante especial (confusamente, fc tiene que ser 0-ary).
Bourbaki, mediante el uso de Hilbert tau de operador (que supongo que es parecido o igual de Hilbert epsilon operador) hace algo similar para permitir que las fórmulas obtenidas por mera contigüidad de la función de los símbolos que aparecen en la separación y reemplazo de los axiomas (ambos enfoques haría que el axioma de elección para ser un teorema), pero por mucho que me guste Bourbaki, he llegado a preferir aquí la forma estándar de los lógicos, de hacer las cosas, que utiliza un axioma de elección. Suponiendo que en exceso no es estéticamente agradable.