Cálculo épsilon

Para cualquier lenguaje formal L , extienda L agregando el operador épsilon para redefinir la cuantificación:

• ${\displaystyle (\exists x)A(x)\ \equiv \ A(\epsilon x\ A)}$
• ${\displaystyle (\forall x)A(x)\ \equiv \ \neg \exists x\neg A(x)\leftrightarrow \neg {\big (}\neg A(\epsilon x\ \neg A){\big )}\leftrightarrow A(\epsilon x\ (\neg A))}$

La interpretación prevista de ϵ x A es algún x que satisface A , si existe. En otras palabras, ϵ x A devuelve algún término t tal que A ( t ) es verdadero; de lo contrario, devuelve algún término predeterminado o arbitrario. Si más de un término puede satisfacer A , entonces cualquiera de estos términos (que hacen que A sea verdadero) puede elegirse de forma no determinista. Se requiere que la igualdad esté definida bajo L , y las únicas reglas requeridas para L extendida por el operador épsilon son el modus ponens y la sustitución de A ( t ) para reemplazar A ( x ) para cualquier término t . ^{[ 2 ]}

En la notación tau-cuadrada de la Teoría de Conjuntos de N. Bourbaki , los cuantificadores se definen de la siguiente manera:

• ${\displaystyle (\exists x)A(x)\ \equiv \ (\tau _{x}(A)|x)A}$
• ${\displaystyle (\forall x)A(x)\ \equiv \ \neg (\tau _{x}(\neg A)|x)\neg A\ \equiv \ (\tau _{x}(\neg A)|x)A}$

donde A es una relación en L , x es una variable y${\displaystyle \tau _{x}(A)}$yuxtapone un${\displaystyle \tau }$al frente de A , reemplaza todas las instancias de x con${\displaystyle \square }$y los vincula de vuelta a${\displaystyle \tau }$. Entonces, sea Y un ensamblaje, (Y|x)A denota la sustitución de todas las variables x en A por Y.

Esta notación es equivalente a la notación de Hilbert y se lee igual. Bourbaki la utiliza para definir la asignación cardinal, ya que no emplea el axioma de reemplazo .

Definir los cuantificadores de esta manera conlleva grandes ineficiencias. Por ejemplo, la expansión de la definición original de Bourbaki del número uno, utilizando esta notación, tiene una longitud aproximada de 4,5 ^× 10¹² , y para una edición posterior de Bourbaki que combinó esta notación con la definición de pares ordenados ^de Kuratowski , este número crece hasta aproximadamente 2,4 × 10⁵⁴ . ^{[ 3 ]}    

Una teoría que se va a comprobar en cuanto a su consistencia se integra primero en un cálculo épsilon apropiado. En segundo lugar, se desarrolla un proceso para reescribir teoremas cuantificados, expresándolos en términos de operaciones épsilon mediante el método de sustitución épsilon. Finalmente, debe demostrarse que el proceso normaliza la reescritura, de modo que los teoremas reescritos satisfagan los axiomas de la teoría. ^{[ 4 ]}