Cálculo épsilon - Epsilon calculus

El cálculo épsilon de Hilbert es una extensión de un lenguaje formal por el operador épsilon, donde el operador épsilon sustituye a los cuantificadores en ese lenguaje como 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 coherencia. El cálculo extendido de épsilon se amplía y generaliza aún más para cubrir aquellos objetos, clases y categorías matemáticos para los que se desea mostrar coherencia, basándose en la coherencia previamente demostrada en niveles anteriores.

Operador de Epsilon

Notación de Hilbert

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

• ${\ Displaystyle (\ existe x) A (x) \ \ equiv \ A (\ epsilon x \ A)}$
• ${\ Displaystyle (\ forall x) A (x) \ \ equiv \ A (\ epsilon x \ (\ neg A))}$

La interpretación pretendida de ϵ x A es una 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 se defina en L , y las únicas reglas requeridas para L extendido por el operador épsilon son modus ponens y la sustitución de A ( t ) para reemplazar A ( x ) por cualquier término t .

Notación Bourbaki

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

• ${\ Displaystyle (\ existe 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 yuxtapone a al principio de A , reemplaza todas las instancias de x con y las vincula de nuevo . Luego dejar que Y sea un montaje, (Y | X) A denota el reemplazo de todas las variables x en A con Y . ${\ Displaystyle \ tau _ {x} (A)}$${\ Displaystyle \ tau}$${\ Displaystyle \ cuadrado}$${\ Displaystyle \ tau}$

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

Definir 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 ¹² , 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 ⁵⁴ .

Enfoques modernos

El programa de Hilbert para las matemáticas era justificar esos sistemas formales como consistentes en relación con los sistemas constructivos o semi-constructivos. Si bien los resultados de Gödel sobre la incompletitud discutieron el Programa de Hilbert en gran medida, los investigadores modernos encuentran que el cálculo épsilon proporciona alternativas para abordar las pruebas de consistencia sistémica como se describe en el método de sustitución épsilon.

Método de sustitución de épsilon

Una teoría cuya coherencia debe comprobarse se integra primero 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.

Ver también

• Álgebra de Clifford : Álgebra ortogonal de finales del siglo XX.
• Gran notación Omega : análisis asintótico analítico y computacional , coincidiendo aproximadamente con el cálculo épsilon y posterior a la fecha, respectivamente.
• Análisis complejo : funciones de variables multiparamétricas anteriores al cálculo épsilon.

Notas

Referencias

• "Epsilon Calculi" . Enciclopedia de Filosofía de Internet .
• Moser, Georg; Richard Zach . El cálculo de Epsilon (Tutorial) . Berlín: Springer-Verlag. OCLC  108629234 .
• Avigad, Jeremy ; Zach, Richard (27 de noviembre de 2013). "El cálculo épsilon" . En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford .
• Bourbaki, N. Teoría de conjuntos . Berlín: Springer-Verlag. ISBN 3-540-22525-0.