Heyting aritmética - Heyting arithmetic
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 . Lleva el nombre de Arend Heyting , quien lo propuso por primera vez.
Introducción
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 (dos números naturales cualesquiera son iguales entre sí o no iguales entre sí). De hecho, dado que "=" es el único símbolo de predicado en la aritmética de Heyting, se deduce que, para cualquier fórmula libre de cuantificadores φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ es un teorema ( donde x , y , z ... son las variables libres en φ ).
Historia
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
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
Referencias
- 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
- 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