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.

DefiniçãoEditar

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:

 

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:

 

  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 yQ 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.

RealizabilidadeEditar

A realizabilidade pode ser usada para justificar o princípio de Markov: um realizador é um operador μ que consecutivamente analisa se   é verdade. Porque   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   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 MarkovEditar

A regra de Markov é a formulação do princípio de Markov como uma regra. Ela declara que   é derivável logo que   seja recursivo para  . 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[1], usando a Tradução de Friedman.

Princípio de Markov fracoEditar

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

 

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.[2]

ReferênciasEditar

  1. 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.
  2. Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.

Ligações externasEditar