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 consistencia para el lenguaje formal extendido. El operador épsilon y el método de sustitución épsilon se aplican típicamente a un cálculo de predicados de primer orden , seguido de una demostración de consistencia. El cálculo épsilon extendido se extiende y generaliza aún más para cubrir aquellos objetos, clases y categorías matemáticos para los que existe un deseo de demostrar consistencia, basándose en la consistencia 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 pretendida de ϵ x A es alguna 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 manera no determinista. Se requiere que la igualdad se defina bajo L , y las únicas reglas requeridas para L extendida por el operador épsilon son modus ponens y la sustitución de A ( t ) para reemplazar A ( x ) por cualquier término t . [2]
En la 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 principio de A , reemplaza todas las instancias de x con , y las vincula de nuevo 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 la utiliza para definir la asignación cardinal, ya que no utiliza 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, utilizando 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 Kuratowski de pares ordenados , este número crece a aproximadamente 2,4 × 10 54 . [3]
El programa de Hilbert para las matemáticas consistía en justificar la coherencia de esos sistemas formales en relación con los sistemas constructivos o semiconstructivos. Si bien los resultados de Gödel sobre la incompletitud cuestionaron en gran medida el programa de Hilbert, los investigadores modernos consideran que el cálculo épsilon ofrece alternativas para abordar las pruebas de coherencia sistémica, como se describe en el método de sustitución épsilon.
En primer lugar, se incorpora una teoría a un cálculo épsilon apropiado para comprobar su coherencia. 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. Por último, 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]
