Aritmética de Heyting

En lógica matemática, se denomina aritmética de Heyting a la axiomatización de la aritmética siguiendo los lineamientos de la escuela intuicionista. El nombre proviene de Arend Heyting, quien fue el primero en proponerla. La aritmética de Heyting adopta los axiomas de Peano, pero utiliza las reglas de inferencia de la lógica intuicionista. Particularmente, el principio del tercero excluido no es en general admitido, pese a que dicho axioma puede ser utilizado para la demostración de algunos casos específicos. Por ejemplo, se puede probar que es un teorema (dos números naturales cualesquiera son o bien iguales o bien no iguales entre sí). En efecto, dado que "=" es el único símbolo de predicado en la aritmética de Heyting, se desprende que, para cualquier proposición p sin cuantificadores es un teorema (donde x,y,z... son variables libres de p). La aritmética de Heyting no debe confundirse con el álgebra de Heyting, que es análogamente el equivalente intuicionista del álgebra de Boole.