En lógica matemática , la aritmética de Heyting (a veces abreviada HA ) es una axiomatización de la aritmética de acuerdo con la filosofía del intuicionismo . [1] Lleva el nombre de Arend Heyting , quien lo propuso por primera vez.
Introducción [ editar ]
La aritmética de Heyting adopta los axiomas de la aritmética de Peano (PA), pero usa la lógica intuicionista como sus reglas de inferencia. En particular, la ley del medio excluido no se cumple en general, aunque el axioma de inducción puede usarse para probar muchos casos específicos. Por ejemplo, se puede probar que ∀ x , y ∈ N : x = y ∨ x ≠ y es un teorema (cualesquiera dos números naturales son iguales entre sí o no iguales entre sí). De hecho, dado que "=" es el único predicadosímbolo en la aritmética de Heyting, se sigue que, para cualquier fórmula libre de cuantificador φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ es un teorema (donde x , y , z ... son los variables libres en φ ).
Historia [ editar ]
Kurt Gödel estudió la relación entre la aritmética de Heyting y la aritmética de Peano. Usó la traducción negativa de Gödel-Gentzen para demostrar en 1933 que si HA es consistente, entonces PA también lo es.
Conceptos relacionados [ editar ]
La aritmética de Heyting no debe confundirse con las álgebras de Heyting , que son el análogo intuicionista de las álgebras de Boole .
Ver también [ editar ]
Referencias [ editar ]
- ↑ Troelstra 1973: 18.
- Ulrich Kohlenbach (2008), Teoría de la prueba aplicada , Springer.
- Anne S. Troelstra , ed. (1973), Investigación metamatemática de aritmética y análisis intuicionistas , Springer, 1973.
Enlaces externos [ editar ]
- Enciclopedia de Filosofía de Stanford : " Teoría intuicionista de los números " por Joan Moschovakis .
- Fragmentos de aritmética de Heyting por Wolfgang Burr
