Principe de Markov

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

${\displaystyle \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 recevable dans l'arithmétique de Heyting. Plus tard, le logicien Harvey Friedman a montré que la règle de Markov est une règle recevable 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.

Si l'arithmétique constructive est traduite à l'aide de la réalisabilité dans une méta-théorie classique qui prouve la ${\displaystyle \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 ${\displaystyle P}$ n'est pas partout fausse à la recherche illimitée qui vérifie successivement si ${\displaystyle P(0),P(1),P(2),\dots }$ est vrai. Si ce ${\displaystyle P}$ n'est pas partout faux, et par ${\displaystyle \omega }$-cohérence il doit y avoir un terme pour lequel ${\displaystyle P}$ est vrai, et chaque terme sera finalement atteint par la recherche. Si toutefois, ${\displaystyle 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), ${\displaystyle 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 le 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.

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

${\displaystyle \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].