Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Heyting arithmetic
Summary
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
Heyting arithmetic can be characterized just like the first-order theory of Peano arithmetic , except that it uses the intuitionistic predicate calculus for inference. In particular, this means that the double-negation elimination principle, as well as the principle of the excluded middle , do not hold. Note that to say does not hold exactly means that the excluded middle statement is not automatically provable for all propositions - indeed many such statements are still provable in and the negation of any such disjunction is inconsistent. is strictly stronger than in the sense that all -theorems are also -theorems.
Heyting arithmetic comprises the axioms of Peano arithmetic and the intended model is the collection of natural numbers . The signature includes zero "" and the successor "", and the theories characterize addition and multiplication. This impacts the logic: With , it is a metatheorem that can be defined as and so that is for every proposition . The negation of is of the form and thus a trivial proposition.
For numbers, write for .
For a fixed number , the equality is true by reflexivity and a proposition is equivalent to .
It may be shown that can then be defined as . This formal elimination of disjunctions was not possible in the quantifier-free primitive recursive arithmetic . The theory may be extended with function symbols for any primitive recursive function, making also a fragment of this theory. For a total function , one often considers predicates of the form .
With explosion valid in any intuitionistic theory, if is a theorem for some , then by definition is provable if and only if the theory is inconsistent. Indeed, in Heyting arithmetic the double-negation explicitly expresses . For a predicate , a theorem of the form expresses that it is inconsistent to rule out that could be validated for some .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.