Arithmétique de Heyting

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

Une proposition indépendante de ${\displaystyle \mathbf {PA} }$ est aussi indépendante de ${\displaystyle \mathbf {HA} }$, puisqu'une preuve de ${\displaystyle P}$ ou ${\displaystyle \neg P}$ dans ${\displaystyle \mathbf {HA} }$ serait aussi valide dans ${\displaystyle \mathbf {PA} }$. Voici plusieurs propositions indépendantes de ${\displaystyle \mathbf {PA} }$ :

• 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 ${\displaystyle \mathbf {PA} }$.
• Le théorème de Matiassevich assure l'existence de polynômes à ${\displaystyle n}$ variables et à coefficients entiers ${\displaystyle f}$ tels que ${\displaystyle \exists x_{1}\dots \exists x_{n}(f(x_{1},\dots ,x_{n})=0)}$ soit indépendante de ${\displaystyle \mathbf {PA} }$.
• 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 ${\displaystyle \mathbf {PA} }$, donc est indépendante de ${\displaystyle \mathbf {PA} }$.
• De même, le théorème de Goodstein est vrai mais non démontrable dans ${\displaystyle \mathbf {PA} }$, donc indépendant de ${\displaystyle \mathbf {PA} }$.

De manière plus générale, on peut montre que si ${\displaystyle \mathbf {HA} \not \vdash P}$ et ${\displaystyle \mathbf {PA} \vdash P}$, ou si ${\displaystyle \mathbf {HA} \not \vdash \neg P}$ et ${\displaystyle \mathbf {PA} \vdash \neg P}$, alors ${\displaystyle P}$ est indépendante de ${\displaystyle \mathbf {HA} }$.

L'arithmétique de Heyting vérifie le principe de disjonction ${\displaystyle \mathrm {DP} }$^[4],[8]. Si ${\displaystyle P}$ et ${\displaystyle Q}$ sont des propositions closes (sans variables libres) :

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 ${\displaystyle P}$, ${\displaystyle P}$ est indépendante de ${\displaystyle \mathbf {HA} }$ si et seulement si ${\displaystyle P\lor \neg P}$ l'est. Une telle proposition ${\displaystyle P}$ fournit ainsi un exemple de propositions pour laquelle le tiers exclu est invalide.

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

L'arithmétique de Peano ne vérifie pas le principe de disjonction. Si ${\displaystyle P}$ est une propriété indépendante de ${\displaystyle \mathbf {PA} }$, par définition ${\displaystyle \mathbf {PA} \not \vdash P}$ et ${\displaystyle \mathbf {PA} \not \vdash \neg P}$ mais ${\displaystyle \mathbf {PA} \vdash P\lor \neg P}$ puisque l'arithmétique de Peano utilise la logique classique.

Si ${\displaystyle T}$ est une théorie récursivement axiomatisable contenant l'arithmétique de Heyting, alors ${\displaystyle T}$ peut exprimer qu'une formule est prouvable dans ${\displaystyle T}$ grâce à un codage de Gödel. Si on note ${\displaystyle \square P}$ la proposition énoncant la démontrabilité de ${\displaystyle P}$, si ${\displaystyle T}$ prouve qu'elle respecte le principe de disjonction, alors ${\displaystyle T}$ prouve qu'elle est incohérente^[9], c'est-à-dire que si ${\displaystyle T\vdash \square (P\lor Q)\implies \square P\lor \square Q}$ pour tout ${\displaystyle P}$ et ${\displaystyle Q}$ alors ${\displaystyle T\vdash \square \bot }$. De plus si ${\displaystyle T}$ respecte le principe de disjonction, alors ${\displaystyle 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, ${\displaystyle \mathbf {HA} }$ ne prouve pas qu'elle respecte le principe de disjonction.

Dans l'arithmétique de Peano, un ensemble définissable ${\displaystyle P}$ ayant au moins un élément possède un plus petit élément :

La formule ${\displaystyle P[x:=y]}$ représente la formule ${\displaystyle P}$ dans laquelle on a substitué ${\displaystyle y}$ à la variable ${\displaystyle x}$. Notons ce principe ${\displaystyle \operatorname {Min} _{P}}$.

Ce principe n'est pas vrai^[10] en général dans l'arithmétique de Heyting. En effet, considérons une formule ${\displaystyle P}$ dans le langage de l'arithmétique, et posons ${\displaystyle Q_{P}=P\lor 0<x}$, avec ${\displaystyle x}$ qui n'est pas libre dans ${\displaystyle P}$. L'arithmétique de Heyting montre que ${\displaystyle Q_{P}}$ est vraie pour ${\displaystyle x=1}$, donc ${\displaystyle \mathbf {HA} \vdash \exists xQ_{P}}$. Supposons que le principe du minimum soit vrai pour ${\displaystyle Q_{P}}$. Alors l'arithmétique de Heyting démontre l'existence d'un élément minimal ${\displaystyle x}$ qui vérifie ${\displaystyle Q_{P}}$. Or ${\displaystyle \mathbf {HA} \vdash Q_{P}[x:=0]\iff P}$ et ${\displaystyle \mathbf {HA} }$ démontre aussi qu'un ${\displaystyle x}$ minimal qui vérifie ${\displaystyle Q_{P}}$ vaut soit ${\displaystyle 0}$ soit ${\displaystyle 1}$. Donc ${\displaystyle \mathbf {HA} \vdash Q_{P}[x:=0]\lor (Q_{P}[x:=1]\land \neg Q_{P}[x:=0])}$, soit ${\displaystyle \mathbf {HA} \vdash P\lor \neg P}$. Or il existe des propositions ${\displaystyle P}$ telles que ${\displaystyle \mathbf {HA} \not \vdash P\lor \neg P}$ : ce sont exactement les propositions indépendantes de ${\displaystyle \mathbf {HA} }$. Pour celles-ci, ${\displaystyle \mathbf {HA} \not \vdash \operatorname {Min} _{P}}$, et ${\displaystyle \operatorname {Min} _{P}}$ est indépendante de ${\displaystyle \mathbf {HA} }$.

Ce qui précède implique l'ordre ${\displaystyle <}$ n'est pas bien fondé dans ${\displaystyle \mathbf {HA} }$. Néanmoins, le principe de récurrence forte reste valide :

Pour le montrer, on applique le principe de récurrence usuelle à la formule ${\displaystyle \forall (k<n)P[x:=k]}$ et à la variable ${\displaystyle 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 :

• (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).

• (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). 
• (en) Applied Proof Theory: Proof Interpretations and their Use in Mathematics (DOI 10.1007/978-3-540-77533-1, lire en ligne).
• (en) Morten Heine Sørensen et Pawel Urzyczyn, Lectures on the Curry-Howard Isomorphism, Elsevier, coll. « Studies in Logic and the Foundations of Mathematics » (n^o 149), 2006, 442 p. (ISBN 9780080478920, lire en ligne). 
• (en) Michael J. Beeson, Foundations of Constructive Mathematics, Heidelberg, Springer Berlin, coll. « Ergebnisse der Mathematik und ihrer Grenzgebiete. A Series of Modern Surveys in Mathematics. » (n^o 3), 2011, 466 p. (ISBN 978-3-642-68954-3, ISSN 0071-1136, DOI 10.1007/978-3-642-68952-9, lire en ligne). 

• Arithmétique

• Axiomes de Peano
• Logique intutionniste

• Portail des mathématiques
• Portail de la logique