Aritmètica de Heyting

En llògica matemàtica, es denomina aritmètica de Heyting a l'axiomatisació de l'aritmètica seguint els lineamientos de l'escola intuicionista. El nom prové d'Arend Heyting, qui va anar el primer en propondre-la.

L'aritmètica de Heyting adopta els axioma de Peano, pero utilisa les regles d'inferència de la llògica intuicionista. Particularment, el principi del tercer exclós no és en general admés, pese a que dit axioma pot ser utilisat per a la demostració d'alguns casos específics. Per eixemple, es pot provar que

$\mathrm{\forall }x,y\in \mathbb{N}:x=y\vee x\ne y$

és un teorema (dos número natural qualssevol són o ben iguals o be no iguals entre sí). En efecte, ya que "=" és l'únic símbol de predicat en l'aritmètica de Heyting, es desprén que, per a qualsevol proposició p sense quantificadorés

$\mathrm{\forall }x,y,z,\mathrm{...}\in \mathbb{N}:p\vee \mathrm{\neg }p$

és una teorema (a on x,i,z... són variables lliures de p).

L'aritmètica de Heyting no deu confondre's en l'àlgebra de Heyting, que és análogamente l'equivalent intuicionista del àlgebra de Boole.