Princípio de Markov

O princípio de Markov, cujo nome advém do matemático Andrei Markov Júnior, filho do também renomado matemático Andrei Markov, é uma tautologia que não é válida por lógica intuicionista mas pode ser justificada por meio de construtivismo. Existem muitas formulações equivalentes ao princípio de Markov.

"Se é impossível que um algoritmo não termine, então ele irá terminar". Uma máquina com uma corrente aparentemente interminável

Definição

Na linguagem da teoria da computabilidade, o princípio de Markov é a expressão do argumento de que, se é impossível que um algoritmo não termine, então ele irá terminar. Isso é equivalente ao argumento de que, se um conjunto e o seu complementar são ambos recursivamente enumeráveis, então o conjunto é recursivo.

Na lógica de predicados, um predicado P sobre um domínio qualquer é chamado recursivo se, para cada x no domínio, ou P(x) é verdadeiro ou P(x) é falso, o que nem sempre é o caso do construtivismo.

Se P é um predicado recursivo sobre os números naturais, o princípio de Markov é expresso como:

$(\forall n(P(n)\vee \neg P(n)))\wedge (\neg \forall n\neg P(n))\rightarrow (\exists n\;P(n)).$

Isto é, se P não pode ser falso para todos os números naturais n, então é verdadeiro para algum n.

Na linguagem de aritmética de Heyting, o princípio é equivalente a:

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

$f$ sendo uma função computável sobre os números naturais.

Na linguagem da análise real, o princípio é equivalente aos seguintes:

• Para cada número real x, se é contraditório que x é igual a 0, então existe um y ∈ Q tal que 0 < y < |x|, muitas vezes expresso por se dizer que x é separado (sugerido do inglês apartness relation ) ou construtivamente diferente de 0.
• Para cada número real x, se é contraditório que x é igual a 0, então existe um y ∈ R tal que xy = 1.

Realizabilidade

A realizabilidade pode ser usada para justificar o princípio de Markov: um realizador é um operador μ que consecutivamente analisa se $P(0),P(1),P(2),\dots$ é verdade. Porque $P$ não é falso em todo lugar, a procura não pode durar para sempre. Usando lógica clássica podemos concluir que a procura termina, nomeadamente, no valor em que $P$ existe.

A realizabilidade modificada não justifica o princípio de Markov, mesmo se a lógica clássica for usada na metateoria: não existe um realizador na linguagem de cálculo lambda simplesmente tipado, haja vista que essa linguagem não é Turing-completa e que ciclos arbitrários não podem ser definidos nela.

Regra de Markov

A regra de Markov é a formulação do princípio de Markov como uma regra. Ela declara que $\exists n\;P(n)$ é derivável logo que $\neg \neg \exists n\;P(n)$ seja recursivo para $P$. O lógico Harvey Friedman mostrou que a regra de Markov é uma regra admissível em lógica intuicionista, aritmética de Heyting e muitas outras teorias intuicionistas, usando a Tradução de Friedman.

Princípio de Markov fraco

Uma forma fraca do princípio de Markov pode ser expressa em linguagem de análise como:

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

Essa forma pode ser justificada pelos princípios da continuidade de Luitzen Egbertus Jan Brouwer, ao passo que a forma mais forte os contradiz. Logo, pode ser derivado do intuicionismo, da realizabilidade e do racionalismo clássico, em cada caso por diferentes razões, mas esse princípio não é valido no sentido lato construtivista de Bishop.

Ligações externas

• Constructive Mathematics (Stanford Encyclopedia of Philosophy)