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 ,\le \}$, 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 auteursModèle:, é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\vee \mathrm{\neg }P$ n'est pas nécessairement démontrable.

On note $𝐇𝐀⊢P$ pour dire que l'arithmétique de Heyting démontre la proposition $P$, et $𝐏𝐀⊢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\vee \mathrm{\neg }P$, ou $\mathrm{\neg }\mathrm{\neg }P⟹P$ ou $\mathrm{\exists }nP⟺\mathrm{\neg }\mathrm{\forall }n\mathrm{\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 Modèle:Centrer

Cette définition correspond à la notion de décidabilité algorithmique du problème « $P$ est-elle logiquement décidable par $𝐇𝐀$ ? ». En effet, dans la correspondance de Curry-Howard, une démonstration de $𝐇𝐀⊢P\vee \mathrm{\neg }P$ correspond à un programme qui produit soit une démonstration de $P$, soit une démonstration de $\mathrm{\neg }P$.

Il ne faut pas confondre cette notion avec celle de décidabilité logique par $𝐇𝐀$ elle-même, qui caractérise les propositions $P$ telles que $𝐇𝐀⊢P$ ou $𝐇𝐀⊢\mathrm{\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 : $𝐇𝐀⊢\mathrm{\forall }x\mathrm{\forall }y(x=y\vee x\ne y)$, ainsi que l'ordre : $𝐇𝐀⊢\mathrm{\forall }x\mathrm{\forall }y(x\le y\vee x\le ̸y)$ (sachant que comme en logique classique, en logique intuitionniste on a équivalence entre une formule et sa Modèle:Lien, 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 : $𝐇𝐀⊢\mathrm{\forall }x\mathrm{\forall }y(x<y\vee x=y\vee x>y)$. On peut montrer que si $P$ est une formule ${\mathrm{\Delta }}_0^0$, $P$ est décidable.

Élimination de la double négation

En logique classique, on a $P⟺\mathrm{\neg }\mathrm{\neg }P$, tandis qu'en logique intuitionniste, seule la version plus faible $P⟹\mathrm{\neg }\mathrm{\neg }P$ est vraie en général. Néanmoins, certaines classes de formules $P$ présentent aussi la propriété $𝐇𝐀⊢\mathrm{\neg }\mathrm{\neg }P⟹P$. C'est en particulier le cas pour les formules décidables et pour les formules de Harrop.

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

• pour les formules ${\mathrm{\Delta }}_0^0$. On le note ${\mathrm{M}\mathrm{P}}_{\mathrm{Q}\mathrm{F}}$.

• pour le prédicat T de Kleene. On le note ${\mathrm{M}\mathrm{P}}_0$.
• pour les prédicats primitifs récursifs. On le note ${\mathrm{M}\mathrm{P}}_{\mathrm{P}\mathrm{R}}$.
• pour les formules décidables, c'est-à-dire pour les formules $P$ telles que $𝐇𝐀⊢P\vee \mathrm{\neg }P$. On le note ${\mathrm{M}\mathrm{P}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$.

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 $𝐇𝐀⊢P$ alors $𝐏𝐀⊢P$. On peut formuler plusieurs réciproques partielles de ce théorème.

Traduction par double négation et équicohérence

Article détaillé : Modèle:Lien

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

• ${\mathrm{\perp }}^{-}=\mathrm{\perp }$ .
• $P^{-}=\mathrm{\neg }\mathrm{\neg }P$ si $P$ est atomique.
• $(P\to Q{)}^{-}=P^{-}\to Q^{-}$.
• $(P\wedge Q{)}^{-}=P^{-}\wedge Q^{-}$.
• $(P\vee Q{)}^{-}=\mathrm{\neg }\mathrm{\neg }(P^{-}\vee Q^{-})$.
• $(\mathrm{\forall }nP{)}^{-}=\mathrm{\forall }n{P}^{-}$.
• $(\mathrm{\exists }nP{)}^{-}=\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }n{P}^{-}$.

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

• Si $𝐏𝐀⊢P$ alors $𝐇𝐀⊢P^{-}$. En particulier si $P$ ne contient ni disjonction ni quantificateur existentiel, $𝐏𝐀⊢P⟺𝐇𝐀⊢P$.
• $𝐏𝐀⊢P⟺P^{-}$.
• $𝐇𝐀⊢\mathrm{\neg }\mathrm{\neg }{P}^{-}⟹P^{-}$.
• $𝐇𝐀⊢(P^{-}{)}^{-}⟺P^{-}$.

On peut aussi montrer que si $P$ est une formule ${\mathrm{\Delta }}_0^0$, $𝐇𝐀⊢P⟺P^{-}$.

Cette traduction a notamment permis à Gödel de montrer l'équicohérence de $𝐏𝐀$ et $𝐇𝐀$ : si $𝐏𝐀⊢\mathrm{\perp }$ alors $𝐇𝐀⊢{\mathrm{\perp }}^{-}$, or ${\mathrm{\perp }}^{-}=\mathrm{\perp }$ donc $𝐇𝐀⊢\mathrm{\perp }$.

Conservativité

En utilisant à la fois la traduction par double-négation, le principe de Markov pour les formules ${\mathrm{\Delta }}_0^0$ et le fait qu'une formule ${\mathrm{\Delta }}_0^0$ est équivalente à sa traduction par double-négation, on peut montrer que l'arithmétique de Peano est conservative par rapport à l'arithmétique de Heyting pour les formules ${\mathrm{\Pi }}_2^0$ : si $P$ est une formule ${\mathrm{\Pi }}_2^0$, alors Modèle:Centrer

Ce résultat implique notamment que si l'arithmétique de Peano démontre qu'une machine de Turing fixée s'arrête quelle que soit son entrée, c'est-à-dire si elle représente une fonction récursive totale, alors l'arithmétique de Heyting le démontre également, puisque si $e$ est un codage de Gödel d'une machine de Turing $M$, le fait que cette machine s'arrête quelle que soit son entrée est la formule ${\mathrm{\Pi }}_0^2$ suivante : $\mathrm{\forall }i\mathrm{\exists }tT(e,i,t)$, où $T$ désigne le prédicat T de Kleene.

Propositions indépendantes

Une proposition $P$ est dite indépendante d'une théorie si cette théorie ne démontre ni $P$, ni sa négation $\mathrm{\neg }P$. Toute proposition indépendante de $𝐏𝐀$ est aussi indépendante de $𝐇𝐀$, mais certaines propositions démontrées par $𝐏𝐀$ sont indépendantes de $𝐇𝐀$. Étant donné qu'une théorie incohérente démontre toutes les propositions, toute cette section supposera la cohérence de $𝐇𝐀$.

Propositions indépendantes de PA

Une proposition indépendante de $𝐏𝐀$ est aussi indépendante de $𝐇𝐀$, puisqu'une preuve de $P$ ou $\mathrm{\neg }P$ dans $𝐇𝐀$ serait aussi valide dans $𝐏𝐀$. Voici plusieurs propositions indépendantes de $𝐏𝐀$ :

• Le paradoxe du menteur, qui est une proposition exprimant qu'elle n'est pas démontrable. La construction d'une telle proposition sert à démontrer le premier théorème de Gödel.
• Le deuxième théorème de Gödel montre que la cohérence de l'arithmétique, exprimée dans l'arithmétique par un codage de Gödel, est indépendante de $𝐏𝐀$.
• Le théorème de Matiassevich assure l'existence de polynômes à $n$ variables et à coefficients entiers $f$ tels que $\mathrm{\exists }{x}_1\dots \mathrm{\exists }{x}_n(f(x_1,\dots ,x_n)=0)$ soit indépendante de $𝐏𝐀$.
• Le théorème de Paris-Harrington montre qu'une certaine version du théorème de Ramsey est vraie mais non démontrable dans $𝐏𝐀$, donc est indépendante de $𝐏𝐀$.
• De même, le théorème de Goodstein est vrai mais non démontrable dans $𝐏𝐀$, donc indépendant de $𝐏𝐀$.

De manière plus générale, on peut montre que si $𝐇𝐀⊬P$ et $𝐏𝐀⊢P$, ou si $𝐇𝐀⊬\mathrm{\neg }P$ et $𝐏𝐀⊢\mathrm{\neg }P$, alors $P$ est indépendante de $𝐇𝐀$.

Principe de disjonction

L'arithmétique de Heyting vérifie le principe de disjonction $\mathrm{D}\mathrm{P}$Modèle:,. Si $P$ et $Q$ sont des propositions closes (sans variables libres) : Modèle:Centrer

Ce principe est vrai pour la logique intuitionniste propositionnel et est qualifié comme étant une bonne propriété pour les théories intuitionnistes. On en déduit que pour tout formule $P$, $P$ est indépendante de $𝐇𝐀$ si et seulement si $P\vee \mathrm{\neg }P$ l'est. Une telle proposition $P$ fournit ainsi un exemple de propositions pour laquelle le tiers exclu est invalide.

De plus, si $P$ est indépendante de $𝐏𝐀$, alors $\mathrm{\neg }P$ est aussi indépendante de $𝐏𝐀$ donc de $𝐇𝐀$, y compris si $P$ et $\mathrm{\neg }\mathrm{\neg }P$ ne sont pas équivalentes dans $𝐇𝐀$. Ceci permet également de conclure que le principe du tiers exclu faible est faux dans $𝐇𝐀$. Ce principe énonce que pour toute proposition $P$, $𝐇𝐀⊢\mathrm{\neg }P\vee \mathrm{\neg }\mathrm{\neg }P$. En revanche, si $P$ n'est indépendante que de $𝐇𝐀$, alors $\mathrm{\neg }P$ n'est pas nécessairement indépendante de $𝐇𝐀$. Par exemple, si $Q$ est indépendante de $𝐇𝐀$, $P=Q\vee \mathrm{\neg }Q$ est indépendante de $𝐇𝐀$ mais pas $\mathrm{\neg }(Q\vee \mathrm{\neg }Q)$ puisque $𝐇𝐀⊢\mathrm{\neg }\mathrm{\neg }(Q\vee \mathrm{\neg }Q)$.

L'arithmétique de Peano ne vérifie pas le principe de disjonction. Si $P$ est une propriété indépendante de $𝐏𝐀$, par définition $𝐏𝐀⊬P$ et $𝐏𝐀⊬\mathrm{\neg }P$ mais $𝐏𝐀⊢P\vee \mathrm{\neg }P$ puisque l'arithmétique de Peano utilise la logique classique.

Si $T$ est une théorie récursivement axiomatisable contenant l'arithmétique de Heyting, alors $T$ peut exprimer qu'une formule est prouvable dans $T$ grâce à un codage de Gödel. Si on note $◻P$ la proposition énoncant la démontrabilité de $P$, si $T$ prouve qu'elle respecte le principe de disjonction, alors $T$ prouve qu'elle est incohérente, c'est-à-dire que si $T⊢◻(P\vee Q)⟹◻P\vee ◻Q$ pour tout $P$ et $Q$ alors $T⊢◻\mathrm{\perp }$. De plus si $T$ respecte le principe de disjonction, alors $T$ est incohérente. Notons que de manière générale, une théorie cohérente peut prouver qu'elle est incohérente. En particulier, $𝐇𝐀$ ne prouve pas qu'elle respecte le principe de disjonction.

Principe du minimum

Dans l'arithmétique de Peano, un ensemble définissable $P$ ayant au moins un élément possède un plus petit élément : Modèle:Centrer La formule $P[x:=y]$ représente la formule $P$ dans laquelle on a substitué $y$ à la variable $x$. Notons ce principe ${\mathrm{Min}}_P$.

Ce principe n'est pas vrai en général dans l'arithmétique de Heyting. En effet, considérons une formule $P$ dans le langage de l'arithmétique, et posons $Q_P=P\vee 0<x$, avec $x$ qui n'est pas libre dans $P$. L'arithmétique de Heyting montre que $Q_P$ est vraie pour $x=1$, donc $𝐇𝐀⊢\mathrm{\exists }x{Q}_P$. Supposons que le principe du minimum soit vrai pour $Q_P$. Alors l'arithmétique de Heyting démontre l'existence d'un élément minimal $x$ qui vérifie $Q_P$. Or $𝐇𝐀⊢Q_P[x:=0]⟺P$ et $𝐇𝐀$ démontre aussi qu'un $x$ minimal qui vérifie $Q_P$ vaut soit $0$ soit $1$. Donc $𝐇𝐀⊢Q_P[x:=0]\vee (Q_P[x:=1]\wedge \mathrm{\neg }{Q}_P[x:=0])$, soit $𝐇𝐀⊢P\vee \mathrm{\neg }P$. Or il existe des propositions $P$ telles que $𝐇𝐀⊬P\vee \mathrm{\neg }P$ : ce sont exactement les propositions indépendantes de $𝐇𝐀$. Pour celles-ci, $𝐇𝐀⊬{\mathrm{Min}}_P$, et ${\mathrm{Min}}_P$ est indépendante de $𝐇𝐀$.

Ce qui précède implique l'ordre $<$ n'est pas bien fondé dans $𝐇𝐀$. Néanmoins, le principe de récurrence forte reste valide : Modèle:Centrer

Pour le montrer, on applique le principe de récurrence usuelle à la formule $\mathrm{\forall }(k<n)P[x:=k]$ et à la variable $n$.

De plus, en utilisant la traduction par double négation, on peut montrer qu'une version plus faible de la propriété du plus petit élément est valide : Modèle:Centrer

Voir aussi

Bibliographie

• Modèle:Ouvrage
• Modèle:Ouvrage.
• Modèle:Ouvrage
• Modèle:Ouvrage

Articles connexes

• Arithmétique

• Axiomes de Peano
• Logique intutionniste