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[modifier | modifier le code]

L'arithmétique de Heyting^[1] 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^[2], tandis que l'arithmétique de Peano est close par déduction logique pour le calcul des prédicats classique. Certains auteurs^[3]^,^[4] é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[modifier | modifier le code]

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[modifier | modifier le code]

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 démonstration de $\mathbf {HA} \vdash P\lor \neg P$ correspond à un programme qui produit soit une démonstration de $P$ , soit une démonstration 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[modifier | modifier le code]

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^[5].

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 démontrable, alors $\exists nP$ aussi. C'est un résultat plus faible que la démontrabilité de $\neg \neg \exists nP\implies \exists nP$ . Ce principe est admissible^[3] 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[modifier | modifier le code]

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[modifier | modifier le code]

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

Kurt Gödel et Gerhard Gentzen ont proposé la traduction^[3] 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^[6] 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é[modifier | modifier le code]

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 l'arithmétique de Peano est conservative^[3] par rapport à l'arithmétique de Heyting pour les formules $\Pi _{2}^{0}$ : 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 démontre qu'une machine de Turing fixée s'arrête quelque 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^[7].

Propositions indépendantes[modifier | modifier le code]

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

Propositions indépendantes de PA[modifier | modifier le code]

Une proposition indépendante de $\mathbf {PA}$ est aussi indépendante de $\mathbf {HA}$ , puisqu'une preuve de $P$ ou $\neg P$ dans $\mathbf {HA}$ serait aussi valide dans $\mathbf {PA}$ . Voici plusieurs propositions indépendantes de $\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 $\mathbf {PA}$ .
Le théorème de Matiassevich assure l'existence de polynômes à $n$ variables et à coefficients entiers $f$ tels que $\exists x_{1}\dots \exists x_{n}(f(x_{1},\dots ,x_{n})=0)$ soit indépendante de $\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 $\mathbf {PA}$ , donc est indépendante de $\mathbf {PA}$ .
De même, le théorème de Goodstein est vrai mais non démontrable dans $\mathbf {PA}$ , donc indépendant de $\mathbf {PA}$ .

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

Principe de disjonction[modifier | modifier le code]

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

\mathbf {HA} \vdash P\lor Q\iff \mathbf {HA} \vdash P\;{\textrm {ou}}\;\mathbf {HA} \vdash Q

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

\mathbf {HA}

si et seulement si

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

L'arithmétique de Peano ne vérifie pas le principe de disjonction. Si $P$ est une propriété indépendante de $\mathbf {PA}$ , par définition $\mathbf {PA} \not \vdash P$ et $\mathbf {PA} \not \vdash \neg P$ mais $\mathbf {PA} \vdash P\lor \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 $\square 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^[9], c'est-à-dire que si $T\vdash \square (P\lor Q)\implies \square P\lor \square Q$ pour tout $P$ et $Q$ alors $T\vdash \square \bot$ . 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, $\mathbf {HA}$ ne prouve pas qu'elle respecte le principe de disjonction.

Principe du minimum[modifier | modifier le code]

Dans l'arithmétique de Peano, un ensemble définissable non vide $P$ possède un plus petit élément :

\mathbf {PA} \vdash \exists xP\implies \exists x(P\land \forall y(y<x\implies \neg P[x:=y]))

La formule $P[x:=y]$ représente la formule $P$ dans laquelle on a substitué $y$ à la variable $x$ . Notons ce principe $\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 $P$ dans le langage de l'arithmétique, et posons $Q_{P}=P\lor 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 $\mathbf {HA} \vdash \exists xQ_{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 $\mathbf {HA} \vdash Q_{P}[x:=0]\iff P$ et $\mathbf {HA}$ démontre aussi qu'un $x$ minimal qui vérifie $Q_{P}$ vaut soit $0$ soit $1$ . Donc $\mathbf {HA} \vdash Q_{P}[x:=0]\lor (Q_{P}[x:=1]\land \neg Q_{P}[x:=0])$ , soit $\mathbf {HA} \vdash P\lor \neg P$ . Or il existe des propositions $P$ telles que $\mathbf {HA} \not \vdash P\lor \neg P$ : ce sont exactement les propositions indépendantes de $\mathbf {HA}$ . Pour celles-ci, $\mathbf {HA} \not \vdash \operatorname {Min} _{P}$ , et $\operatorname {Min} _{P}$ est indépendante de $\mathbf {HA}$ .

Notes et références[modifier | modifier le code]

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

↑ Heyting 1971, p. 13-15.
↑ Heyting 1971, p. 101-109.
↑ ^{a b c et d} (en) Harvey Friedman, « Classically and intuitionistically provably recursive functions », Higher Set Theory, Springer,‎ 1978, p. 21–27 (ISBN 978-3-540-35749-0, DOI 10.1007/BFb0103100, lire en ligne, consulté le 12 mai 2024)
↑ ^{a et b} Sørensen et Urzyczyn 2006, p. 174.
↑ (en) R. Harrop, « On disjunctions and existential statements in intuitionistic systems of logic », Mathematische Annalen, vol. 132, n^o 4,‎ 1^er août 1956, p. 347–361 (ISSN 1432-1807, DOI 10.1007/BF01360048, lire en ligne, consulté le 17 mai 2024)
↑ (de) Kurt Gödel, « Zur intuitionistischen Arithmetik und Zahlentheorie », Ergebnisse eines mathematischen Kolloquiums, vol. 4,‎ 1933, p. 34-38
↑ Sørensen et Urzyczyn 2006, p. 175.
↑ Beeson 2011, p. 156.
↑ (en) Harvey Friedman, « The disjunction property implies the numerical existence property », Proceedings of the National Academy of Sciences, vol. 72, n^o 8,‎ août 1975, p. 2877–2878 (ISSN 0027-8424 et 1091-6490, PMID 16592266, PMCID PMC432880, DOI 10.1073/pnas.72.8.2877, lire en ligne, consulté le 22 mai 2024)
↑ (en) Makoto Fujiwara et Taishi Kurahashi, « Refining the arithmetical hierarchy of classical principles », Mathematical Logic Quarterly, vol. 68, n^o 3,‎ août 2022, p. 318–345 (ISSN 0942-5616 et 1521-3870, DOI 10.1002/malq.202000077, arXiv https://arxiv.org/abs/2010.11527)

Voir aussi[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

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

Articles connexes[modifier | modifier le code]

Arithmétique

[1] Heyting 1971, p. 13-15.

[2] Heyting 1971, p. 101-109.

[:0-3] {a b c et d} (en) Harvey Friedman, « Classically and intuitionistically provably recursive functions », Higher Set Theory, Springer,‎ 1978, p. 21–27 (ISBN 978-3-540-35749-0, DOI 10.1007/BFb0103100, lire en ligne, consulté le 12 mai 2024)

[:1-4] {a et b} Sørensen et Urzyczyn 2006, p. 174.

[5] (en) R. Harrop, « On disjunctions and existential statements in intuitionistic systems of logic », Mathematische Annalen, vol. 132, n^o 4,‎ 1^er août 1956, p. 347–361 (ISSN 1432-1807, DOI 10.1007/BF01360048, lire en ligne, consulté le 17 mai 2024)

[6] (de) Kurt Gödel, « Zur intuitionistischen Arithmetik und Zahlentheorie », Ergebnisse eines mathematischen Kolloquiums, vol. 4,‎ 1933, p. 34-38

[7] Sørensen et Urzyczyn 2006, p. 175.

[8] Beeson 2011, p. 156.

[9] (en) Harvey Friedman, « The disjunction property implies the numerical existence property », Proceedings of the National Academy of Sciences, vol. 72, n^o 8,‎ août 1975, p. 2877–2878 (ISSN 0027-8424 et 1091-6490, PMID 16592266, PMCID PMC432880, DOI 10.1073/pnas.72.8.2877, lire en ligne, consulté le 22 mai 2024)

[10] (en) Makoto Fujiwara et Taishi Kurahashi, « Refining the arithmetical hierarchy of classical principles », Mathematical Logic Quarterly, vol. 68, n^o 3,‎ août 2022, p. 318–345 (ISSN 0942-5616 et 1521-3870, DOI 10.1002/malq.202000077, arXiv https://arxiv.org/abs/2010.11527)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]