Heyting arithmetic

In mathematical logic, Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.^[1] It is named after Arend Heyting, who first proposed it.