Principe de Markov

Le principe de Markov, nommé d'après Andreï Markov Jr, est une déclaration d'existence conditionnelle pour laquelle il existe de nombreuses formulations, ainsi qu'il est discuté ci-dessous.

Ce principe est utilisé dans la validité logique classique, mais pas dans les mathématiques intuitionniste constructives. Toutefois, de nombreux cas particuliers sont prouvables dans un contexte constructif.

Histoire

Le principe a d'abord été étudié et adopté par l'école russe du constructivisme, généralement avec l'axiome du choix dépendant et souvent avec une approche réalisable de la notion de fonction mathématique.

Dans la théorie de la calculabilité

Dans le langage de la théorie de la calculabilité, le principe de Markov est l'expression formelle de l'idée que s'il est impossible qu'un algorithme ne termine pas, alors il doit terminer. C'est l'équivalent de l'idée que si un ensemble et son complémentaire sont tous les deux énumérables, alors cet ensemble est décidable.

Dans la logique intuitionniste

Dans la logique des prédicats, un prédicat P sur un domaine est appelé décidable si pour tout x dans ce domaine, alors ou bien P(x) est vrai, ou bien P(x) n'est pas vrai. Ce n'est pas trivialement vrai de manière constructive.

Pour un prédicat décidable P sur les nombres naturels, le principe de Markov s'énonce ainsi :

(\forall n(P(n)\vee \neg P(n))\wedge \neg \forall n\,\neg P(n))\rightarrow \exists n\,P(n)

C'est-à-dire, si P ne peut pas être faux pour tous les nombres naturels, alors il est vrai pour un certain n.

Règle de Markov

La règle de Markov est la formulation du principe Markov comme une règle. Elle stipule que pour $P$ un prédicat décidable $\exists n\;P(n)$ est dérivable dès lors que $\neg \neg \exists n\;P(n)$ l'est. Formellement :

\forall n(P(n)\lor \neg P(n)),\ \neg \neg \exists n\;P(n)\ \vdash \ \exists n\;P(n)

Anne S. Troelstra^[1] a prouvé qu'il s'agit d'une règle admissible dans l'arithmétique de Heyting. Plus tard, le logicien Harvey Friedman a montré que la règle de Markov est une règle admissible dans l'ensemble de la logique intuitionniste, dans l'arithmétique de Heyting, ainsi que divers autres théories intuitionnistes^[2], en s'appuyant sur la traduction de Friedman.

Dans l'arithmétique de Heyting

Dans le langage de l'arithmétique, le principe peut s'énoncer ainsi :

\neg \neg \exists n\;f(n)=0\rightarrow \exists n\;f(n)=0,

pour $f$ une fonction récursive totale sur les nombres naturels.

Réalisabilité

Si l'arithmétique constructive est traduite à l'aide de la réalisabilité dans une méta-théorie classique qui prouve la $\omega$ -cohérence de la théorie classique (par exemple, l'arithmétique de Peano, si nous sommes à l'étude de l'arithmétique de Heyting), alors le principe de Markov est justifié : un réalisateur est la fonction constante qui prend une réalisation que $P$ n'est pas partout fausse à la recherche illimitée qui vérifie successivement si $P(0),P(1),P(2),\dots$ est vrai. Si ce $P$ n'est pas partout faux, et par $\omega$ -cohérence il doit y avoir un terme pour lequel $P$ est vrai, et chaque terme sera finalement atteint par la recherche. Si toutefois, $P$ n'est pas vrai quelque part, alors le domaine de la fonction constante doit être vide, si bien que, même si la recherche ne s'arrêtera pas, il est toujours vrai de façon vide que la fonction est un réalisateur. Par la Loi du tiers Exclu (dans notre méta-théorie classique), $P$ doit détenir nulle part ou de ne pas tenir nulle part, donc cette fonction constante est un réalisateur.

Si, au contraire, l'interprétation de la réalisabilité est utilisé dans un esprit constructif de la méta-théorie, alors le principe de Markov n'est pas justifié. En effet, pour l'arithmétique du premier ordre, il capture exactement la différence entre un esprit constructif et un esprit classique de la méta-théorie. Plus précisément, une déclaration est démontrable dans l'arithmétique de Heyting avec la thèse étendue de Church si et seulement si il existe un nombre qui réalise cette preuve dans l'arithmétique de Heyting; et ceci est démontrable dans l'arithmétique de Heyting avec la thèse de Church étendue et le principe de Markov si et seulement s'il existe un nombre qui réalise cette preuve dans l'arithmétique de Peano.

Dans l'analyse constructive

Il est l'équivalent dans le langage de l'analyse réelle, aux principes suivants:

Pour tout nombre réel x, s'il est contradictoire que x est égal à 0, alors il existe y ∈ Q tel que 0 < y < |x|, souvent exprimé en disant que x est séparé de 0, ou inégal à 0 de manière constructive.
Pour tout nombre réel x, s'il est contradictoire que x est égal à 0, alors il existe y ∈ R tel que xy = 1.

La réalisabilité modifiée ne justifie pas le principe de Markov, même si la logique classique est utilisé dans la méta-théorie : il n'y a pas de réalisateur dans le langage du lambda-calcul simplement typé puisque ce langage n'est pas Turing-complet et que des boucles arbitraires ne peuvent y être définies.

Le principe de Markov faible

Le principe de Markov faible est une forme plus faible du principe de Markov pouvant être énoncé dans le langage de l'analyse comme

\forall x\in \mathbb {R} \ \ (\forall y\in \mathbb {R} \ \ \neg \neg (0<y)\vee \neg \neg (y<x))\to 0<x.

C'est une déclaration conditionnelle sur la decidabilité de la positivité d'un nombre réel.

Cette forme peut être justifiée par les principes de continuité de Brouwer, tandis que la forme plus forte les contredit. Ainsi, il peut être dérivée à partir de raisonnements en logiques intuitionniste, réalisable et classique, dans chaque cas, pour des raisons différentes. Mais ce principe n'est pas valable dans le grand sens constructif de Bishop^[3].

Voir aussi

Références

↑ Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Verlag (1973), Theorem 4.2.4 of the 2nd edition.
↑ Harvey Friedman. Classically and Intuitionistically Provably Recursive Functions. In Scott, D. S. and Muller, G. H. Editors, Higher Set Theory, Volume 699 of Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28.
↑ Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.

Liens externes

Mathématiques constructives (Stanford Encyclopedia of philosophy) (en anglais)

[1] Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Verlag (1973), Theorem 4.2.4 of the 2nd edition.

[2] Harvey Friedman. Classically and Intuitionistically Provably Recursive Functions. In Scott, D. S. and Muller, G. H. Editors, Higher Set Theory, Volume 699 of Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28.

[3] Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.

[1]

[2]

[3]