Principe de Markov

vignette|250x250px|Une représentation artistique d'une machine de Turing. Le principe de Markov dit que s'il est impossible qu'une machine de Turing ne s'arrête pas, alors elle doit s'arrêter. 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. 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 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 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 : C'est-à-dire, si P ne peut pas être faux pour tous les nombres naturels, alors il est vrai pour un certain n. La règle de Markov est la formulation du principe Markov comme une règle. Elle stipule que pour un prédicat décidable est dérivable dès lors que l'est. Formellement : Anne S. Troelstra 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, en s'appuyant sur la traduction de Friedman.