Arithmétique de Heyting

L'arithmétique de Heyting est une axiomatisation de l'arithmétique dans le cadre de la logique intutionniste. Elle a été développée à l'origine par Arend Heyting.

Définition

L'arithmétique de Heyting est une théorie du premier ordre égalitaire sur la signature $\{0,S,+,\times ,\leq \}$, dont les axiomes sont les axiomes de Peano, close par déduction logique pour le calcul des prédicats intuitionniste, tandis que l'arithmétique de Peano est close par déduction logique pour le calcul des prédicats classique. Certains auteurs étendent le langage de l'arithmétique avec des symboles de fonctions pour chaque fonction primitive récursive.

En particulier, dans l'arithmétique de Heyting, si $P$ est une formule quelconque, $P\lor \neg P$ n'est pas nécessairement démontrable.

On note $\mathbf {HA} \vdash P$ pour dire que l'arithmétique de Heyting démontre la proposition $P$, et $\mathbf {PA} \vdash P$ pour dire que l'arithmétique de Peano démontre $P$.

Propriétés logiques

Certains principes logiques valides en logique classique ne sont pas valides en logique intuitionniste. En effet, de manière générale, $P\lor \neg P$, ou $\neg \neg P\implies P$ ou $\exists nP\iff \neg \forall n\neg P$ sont démontrables en logique classique mais pas en logique intuitionniste. Néanmoins, pour certaines formules en particulier, ces principes peuvent être vrais.

Décidabilité et tiers exclu

Une formule $P$ est dite décidable si $\mathbf {HA} \vdash P\lor \neg P$. Cette définition correspond à la notion de décidabilité algorithmique du problème « $P$ est-elle logiquement décidable par $\mathbf {HA}$ ? ». En effet, dans la correspondance de Curry-Howard, une preuve de $\mathbf {HA} \vdash P\lor \neg P$ correspond à un programme qui produit soit une preuve de $P$, soit une preuve de $\neg P$. Il ne faut pas confondre cette notion avec celle de décidabilité logique par $\mathbf {HA}$ elle-même, qui caractérise les propositions $P$ telles que $\mathbf {HA} \vdash P$ ou $\mathbf {HA} \vdash \neg P$ indépendamment de la décidabilité algorithmique ou non de cette question.

En logique classique, toutes les formules sont décidables : c'est le tiers exclu. L'arithmétique de Heyting démontre que l'égalité est décidable : $\mathbf {HA} \vdash \forall x\forall y(x=y\lor x\neq y)$, ainsi que l'ordre : $\mathbf {HA} \vdash \forall x\forall y(x\leq y\lor x\not \leq y)$ (sachant que comme en logique classique, en logique intuitionniste on a équivalence entre une formule et sa clôture universelle (en), ces assertions en sont bien de décidabilité suivant la définition donnée ci-dessus, les quantifications universelles n’y étant qu’accessoires à équivalence près). De plus l'arithmétique de Heyting vérifie le principe de trichotomie : $\mathbf {HA} \vdash \forall x\forall y(x<y\lor x=y\lor x>y)$. On peut montrer que si $P$ est une formule $\Delta _{0}^{0}$, $P$ est décidable.

Élimination de la double négation

En logique classique, on a $P\iff \neg \neg P$, tandis qu'en logique intuitionniste, seule la version plus faible $P\implies \neg \neg P$ est vraie en général. Néanmoins, certaines classes de formules $P$ présentent aussi la propriété $\mathbf {HA} \vdash \neg \neg P\implies P$. C'est en particulier le cas pour les formules décidables et pour les formules de Harrop (en).

On peut également formuler une réciproque faible de l'élimination de la double négation pour les formules $\Sigma _{1}^{0}$. Le principe de Markov énonce que si $\neg \neg \exists nP$ est prouvable, alors $\exists nP$ aussi. C'est un résultat plus faible que la prouvabilité de $\neg \neg \exists nP\implies \exists nP$. Ce principe est admissible pour un certain nombre de classes de formules $P$ :

• pour les formules $\Delta _{0}^{0}$. On le note $\mathrm {MP} _{\mathrm {QF} }$.

• pour le prédicat T de Kleene (en). On le note $\mathrm {MP} _{0}$.
• pour les prédicats primitifs récursifs. On le note $\mathrm {MP} _{\mathrm {PR} }$.
• pour les formules décidables, c'est-à-dire pour les formules $P$ telles que $\mathbf {HA} \vdash P\lor \neg P$. On le note $\mathrm {MP} _{\mathrm {Dec} }$.

Liens avec l'arithmétique de Peano

Les règles de déduction de la logique intuitionniste étant valides en logique classique, tout théorème de l'arithmétique de Heyting est aussi un théorème de l'arithmétique de Peano : si $\mathbf {HA} \vdash P$ alors $\mathbf {PA} \vdash P$. On peut formuler plusieurs réciproques partielles de ce théorème.

Traduction par double-négation et équicohérence

Article détaillé : non-non traduction (en)

Kurt Gödel et Gerhard Gentzen ont proposé la traduction suivante $P^{-}$ d'une formule $P$ :

• $\bot ^{-}=\bot$ .
• $P^{-}=\neg \neg P$ si $P$ est atomique.
• $(P\to Q)^{-}=P^{-}\to Q^{-}$.
• $(P\land Q)^{-}=P^{-}\land Q^{-}$.
• $(P\lor Q)^{-}=\neg \neg (P^{-}\lor Q^{-})$.
• $(\forall nP)^{-}=\forall nP^{-}$.
• $(\exists nP)^{-}=\neg \neg \exists nP^{-}$.

Cette traduction possède les propriétés suivantes :

• Si $\mathbf {PA} \vdash P$ alors $\mathbf {HA} \vdash P^{-}$. En particulier si $P$ ne contient ni disjonction ni quantificateur existentiel, $\mathbf {PA} \vdash P\iff \mathbf {HA} \vdash P$.
• $\mathbf {PA} \vdash P\iff P^{-}$.
• $\mathbf {HA} \vdash \neg \neg P^{-}\implies P^{-}$.
• $\mathbf {HA} \vdash (P^{-})^{-}\iff P^{-}$.

On peut aussi montrer que si $P$ est une formule $\Delta _{0}^{0}$, $\mathbf {HA} \vdash P\iff P^{-}$.

Cette traduction a notamment permis à Gödel de montrer l'équicohérence de $\mathbf {PA}$ et $\mathbf {HA}$ : si $\mathbf {PA} \vdash \bot$ alors $\mathbf {HA} \vdash \bot ^{-}$, or $\bot ^{-}=\bot$ donc $\mathbf {HA} \vdash \bot$.

Conservativité

En utilisant à la fois la traduction par double-négation, le principe de Markov pour les formules $\Delta _{0}^{0}$ et le fait qu'une formule $\Delta _{0}^{0}$ est équivalente à sa traduction par double-négation, on peut montrer que si $P$ est une formule $\Pi _{2}^{0}$, alors $\mathbf {PA} \vdash P\iff \mathbf {HA} \vdash P$.

Ce résultat implique notamment que si l'arithmétique de Peano prouve qu'une machine de Turing s'arrête quelque soit son entrée, alors l'arithmétique de Heyting le prouve également.

Notes et références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Heyting arithmetic » (voir la liste des auteurs).

Voir aussi

Bibliographie

• (en) Arend Heyting, Intuitionism: An Introduction, Amsterdam, North-Holland Publishing Company, 1971, 3^e éd. (1^re éd. 1956) (ISBN 978-0-7204-2239-9). 

Articles connexes

• Arithmétique

• Axiomes de Peano
• Logique intutionniste