En lógica matemática, la teoría de la igualdad pura es una teoría de primer orden . Tiene una firma que consiste únicamente en el símbolo de la relación de igualdad y no incluye ningún axioma no lógico. [1]
Esta teoría es consistente pero incompleta, ya que un conjunto no vacío con la relación de igualdad habitual proporciona una interpretación que hace que ciertas oraciones sean verdaderas. Es un ejemplo de una teoría decidible y es un fragmento de teorías decidibles más expresivas, incluida la clase monádica de lógica de primer orden (que también admite predicados unarios y está, a través de la forma normal de Skolem , relacionada [2] con las restricciones de conjuntos en el análisis de programas ) y la teoría monádica de segundo orden de un conjunto puro (que además permite la cuantificación sobre predicados y cuya firma se extiende a la lógica monádica de segundo orden de k sucesores [3] ).
Leopold Löwenheim demostró en 1915 que la teoría de la igualdad pura era decidible .
Si se añade un axioma adicional que diga que hay exactamente m objetos para un número natural fijo m , o se añade un esquema axiomático que diga que hay infinitos objetos, entonces la teoría resultante está completa .
La teoría pura de la igualdad contiene fórmulas de lógica de primer orden con igualdad, donde el único símbolo de predicado es la igualdad misma y no hay símbolos de función.
En consecuencia, la única forma de una fórmula atómica es donde son variables (posiblemente idénticas). Se pueden construir fórmulas sintácticamente más complejas como es habitual en la lógica de primer orden utilizando conectores proposicionales como y cuantificadores .
Una estructura de primer orden con igualdad que interpreta tales fórmulas es simplemente un conjunto con la relación de igualdad en sus elementos. Las estructuras isomorfas con tal firma son, por lo tanto, conjuntos de la misma cardinalidad . La cardinalidad, por lo tanto, determina de manera única si una oración es verdadera en la estructura.
La siguiente fórmula:
es verdadero cuando el conjunto que interpreta la fórmula tiene como máximo dos elementos.
Esta teoría puede expresar el hecho de que el dominio de interpretación tiene al menos elementos para una constante utilizando la fórmula que denotaremos para una constante :
Mediante la negación, se puede expresar que el dominio tiene más de elementos. En términos más generales, se puede restringir el dominio a un conjunto finito dado de cardinalidades finitas.
En términos de modelos, la teoría pura de la igualdad puede definirse como el conjunto de aquellas proposiciones de primer orden que son verdaderas para todos los conjuntos (no vacíos), independientemente de su cardinalidad. Por ejemplo, la siguiente es una fórmula válida en la teoría pura de la igualdad:
Por la completitud de la lógica de primer orden, todas las fórmulas válidas son demostrables utilizando axiomas de la lógica de primer orden y los axiomas de igualdad (ver también lógica ecuacional ).
La decidibilidad se puede demostrar estableciendo que cada oración puede demostrarse equivalente a una combinación proposicional de fórmulas sobre la cardinalidad del dominio. [4]
Para obtener la eliminación de cuantificadores , se puede expandir la firma del lenguaje mientras se preservan las relaciones definibles (una técnica que funciona de manera más general para fórmulas monádicas de segundo orden). Otro enfoque para establecer la decidibilidad es utilizar juegos de Ehrenfeucht–Fraïssé .
