Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Heyting arithmetic
Résumé
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 .
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.