En lógica, el cálculo épsilon de Hilbert es una extensión de un lenguaje formal mediante el operador épsilon, donde el operador épsilon sustituye a los cuantificadores en ese lenguaje como un método que conduce a una prueba de coherencia para el lenguaje formal extendido. El operador épsilon y el método de sustitución épsilon generalmente se aplican a un cálculo de predicados de primer orden , seguido de una demostración de coherencia. El cálculo extendido épsilon se extiende y generaliza aún más para cubrir aquellos objetos, clases y categorías matemáticas para las cuales existe el deseo de mostrar coherencia, basándose en la coherencia demostrada previamente en niveles anteriores. [1]
Para cualquier lenguaje formal L , extienda L agregando el operador épsilon para redefinir la cuantificación:
La interpretación prevista de ϵ x A es alguna x que satisfaga A , si existe. En otras palabras, ϵ x A devuelve algún término t tal que A ( t ) sea 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 manera no determinista. Se requiere que la igualdad se defina bajo L , y las únicas reglas requeridas para L extendidas por el operador épsilon son el modus ponens y la sustitución de A ( t ) para reemplazar A ( x ) por cualquier término t . [2]
En notación tau-cuadrado de la Teoría de conjuntos de N. Bourbaki , los cuantificadores se definen de la siguiente manera:
donde A es una relación en L , x es una variable y yuxtapone a al frente de A , reemplaza todas las instancias de x con y las vincula nuevamente a . Entonces sea Y un conjunto, (Y|x)A denota el reemplazo de todas las variables x en A con Y .
Esta notación es equivalente a la notación de Hilbert y se lee igual. Bourbaki lo utiliza para definir la asignación cardinal ya que no utilizan el axioma de reemplazo .
Definir los cuantificadores de esta manera conduce a grandes ineficiencias. Por ejemplo, la expansión de la definición original de Bourbaki del número uno, usando esta notación, tiene una longitud de aproximadamente 4,5 × 10 12 , 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 54 . [3]
El programa de Hilbert para las matemáticas consistía en justificar esos sistemas formales como consistentes en relación con los sistemas constructivos o semiconstructivo. Si bien los resultados de Gödel sobre la incompletitud cuestionaron en gran medida el programa de Hilbert, los investigadores modernos encuentran que el cálculo épsilon proporciona alternativas para acercarse a las pruebas de consistencia sistémica como se describe en el método de sustitución épsilon.
Primero se integra una teoría cuya coherencia se va a comprobar en un cálculo épsilon apropiado. En segundo lugar, se desarrolla un proceso para reescribir teoremas cuantificados que se expresarán en términos de operaciones épsilon mediante el método de sustitución épsilon. Finalmente, se debe demostrar que el proceso normaliza el proceso de reescritura, de modo que los teoremas reescritos satisfagan los axiomas de la teoría. [4]
