Math 2.0

Mathematical logic and foundations Constructive mathematics Concept

Heyting arithmetic

Builds on Peano axiomsIntuitionistic logic

Summary

Heyting arithmetic, HA, is the theory of the natural numbers with the axioms of Peano arithmetic and the rules of intuitionistic logic. It is the standard formal system for constructive arithmetic. Every existence theorem of HA comes with a way to compute a witness. It proves the same formulas as Peano arithmetic up to a double-negation translation, so the two theories are equally consistent.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph
Intuitionistic logic, concept, no evidence levelIntuitionistic logicconceptPeano axioms, concept, no evidence levelPeano axiomsconceptHeyting arithmetic, concept, no evidence levelHeyting arithmeticconcept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Intuitionistic logic concept
  2. Peano axioms concept
  3. Heyting arithmetic concept

Where this leads

5 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Heyting_arithmetic
About this page
TagCK8ZQRN183
URIm2://CK8ZQRN183
Kindconcept
WritingW0 stub
MSC03F55, 03F30, 03F50
UsesPeano axioms, Intuitionistic logic
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by

Definitions