La lógica de primer orden se puede definir con o sin la igualdad. Si usted está trabajando en una lógica de primer orden con igualdad, que es el caso típico, que indica que el $X = Y \iff \forall x.x\in X\Leftrightarrow x \in Y$ es una gran axioma que podría llevar a la contradicción. El beneficio de trabajar en una lógica de la igualdad es que tienes la regla de sustitución es igual para los iguales en los predicados. Como bof mencionado, este es el indiscernibility de identicals $\cfrac{x = y\qquad P(x)}{P(y)}$. Tener la igualdad como parte de la lógica también afecta a la semántica (aunque teniendo en cuenta los modelos de la teoría de conjuntos no es una cosa que uno hace normalmente a menos de que se trata de un conjunto teórico). Si la igualdad es parte de la lógica, entonces exigimos igualdad en realidad ser la igualdad en la semántica.
Si, por el contrario, se utiliza una lógica de primer orden sin igualdad, a continuación, $=$ es sólo otro predicado binario símbolo como cualquier otro. No es diferente de la $\in$. En este caso, el "axioma" de extensionality es simplemente su definición. El indiscernibility de identicals es ahora un meta-teorema que usted necesita para probar, y fácilmente podría no ser cierto. Esto no sería un problema, pero significaría que el $=$ relación no se comportan como la igualdad. (Una vez más, el contraste, en FOL con la igualdad, un fracaso de la indiscernibility de identicals sería una contradicción.) Semánticamente, $=$ acaba de ser modelado como una relación de equivalencia que era compatible con $\in$.
Así que si el "axioma de la extensibilidad" es no trivial de la lógica de afirmación o una definición depende de si la igualdad ya está definido o no. En FOL con la igualdad, es y por lo tanto este es un axioma que, muy posiblemente, podría causar una contradicción. En FOL sin igualdad, esto es simplemente una definición de una relación binaria símbolo y no puede causar la contradicción; sólo puede ser engañosa. Debo decir que desde la perspectiva de la informal de las pruebas, no hace ninguna diferencia de la visión que usted toma. Para más pruebas, si se puede usar el meta-teorema de probar la indiscernibility de identicals, entonces tampoco va a ser muy diferente, pero que el meta-teorema sólo significa que una real prueba formal existe. El real de la prueba formal puede ser bastante grande donde, si estábamos trabajando en una lógica de la igualdad, sería a un solo paso de inferencia. Esto sería un problema para un mecanizado de la aplicación de la lógica, o si usted quiere realmente escribir la prueba formal. En este sentido, trabajar en una lógica de la igualdad es mucho más conveniente.
