Princípio de Markov

O Princípio de Markov , em homenagem a Andrei Markov Jr , é uma declaração de existência condicional para a qual existem muitas formulações, conforme discutido abaixo.

Este princípio é usado na validade lógica clássica, mas não na matemática intuicionista construtiva . No entanto, muitos casos especiais podem ser provados em um contexto construtivo.

História

O princípio foi estudado e adotado pela primeira vez pela escola russa de construtivismo, geralmente com o axioma da escolha dependente e, muitas vezes, com uma abordagem viável da noção de função matemática.

Na teoria da computabilidade

Na linguagem da teoria da computabilidade , o princípio de Markov é a expressão formal da ideia de que, se é impossível para um algoritmo não terminar, ele deve terminar. É o equivalente à ideia de que se um conjunto e seu complemento são enumeráveis , então esse conjunto é decidível .

Na lógica Intuicionista

Na lógica dos predicados , um predicado P em um domínio é denominado decidível se, para todo x neste domínio, P ( x ) for verdadeiro ou P ( x ) não for verdadeiro. Isso não é trivialmente verdade de uma forma construtiva.

Para um predicado decidível P em números naturais , o princípio de Markov é afirmado da seguinte forma:

{\ displaystyle (\ forall n (P (n) \ vee \ neg P (n)) \ wedge \ neg \ forall n \, \ neg P (n)) \ rightarrow \ existe n \, P (n)}

Ou seja, se P não pode ser falso para todos os números naturais, então é verdadeiro para alguns n .

Regra de Markov

A regra de Markov é a formulação do princípio de Markov como regra. Afirma que, para um predicado decidível, é derivável enquanto for. Formalmente: $P$ ${\ displaystyle \ existe n \; P (n)}$ ${\ displaystyle \ neg \ neg \ existe n \; P (n)}$

{\ displaystyle \ forall n (P (n) \ lor \ neg P (n)), \ \ neg \ neg \ existe n \; P (n) \ \ vdash \ \ existe n \; P (n)}

Anne S. Troelstra provou que esta é uma regra válida na aritmética de Heyting. Mais tarde, o lógico Harvey Friedman mostrou que a regra de Markov é uma regra admissível em toda a lógica intuicionista , na aritmética de Heyting, bem como em várias outras teorias intuicionistas, baseando-se na tradução de Friedman.

Na aritmética de Heyting

Na linguagem da aritmética, o princípio pode ser expresso da seguinte forma:

{\ displaystyle \ neg \ neg \ existe n \; f (n) = 0 \ rightarrow \ existe n \; f (n) = 0,}

para uma função recursiva total sobre números naturais. $f$

Realizabilidade

Se a aritmética construtiva é traduzida usando a viabilidade em uma metateoria clássica que prova a consistência da teoria clássica (por exemplo, a aritmética de Peano, se estivermos estudando a aritmética de Heyting), então o princípio de Markov é justificado: um realizador é a função constante que assume um realização que não é falsa em toda parte com a busca ilimitada que verifica sucessivamente se é verdadeira. Se isso não estiver errado em todos os lugares, e por consistência, deve haver um termo para o qual é verdadeiro, e cada termo acabará sendo correspondido pela pesquisa. Se, no entanto, não for verdadeiro em algum lugar, então o domínio da função constante deve estar vazio, de modo que, embora a pesquisa não pare, ainda seja totalmente verdadeiro que a função é um implementador. Pela Lei do Terceiro Excluído (em nossa metateoria clássica), não deve valer em lugar nenhum ou não valer em lugar nenhum, então esta função constante é um realizador. $\ómega$ $P$ ${\ displaystyle P (0), P (1), P (2), \ dots}$ $P$ $\ómega$ $P$ $P$ $P$

Se, ao contrário, a interpretação de realizável é usada em um espírito construtivo de metateoria, então o princípio de Markov não se justifica. Na verdade, para a aritmética de primeira ordem, ele captura exatamente a diferença entre uma mente construtiva e uma mente clássica de metateoria. Mais precisamente, uma declaração pode ser demonstrada na aritmética de Heyting com a tese estendida de Church se e somente se houver um número que atinja essa prova na aritmética de Heyting; e isso é demonstrável na aritmética de Heyting com a tese estendida de Church e o princípio de Markov se e somente se houver um número que atinja essa prova na aritmética de Peano .

Em análise construtiva

É o equivalente, na linguagem da análise real , aos seguintes princípios:

Para qualquer número real x , se for contraditório que x seja igual a 0, então existe y ∈ Q tal que 0 < y <| x |, geralmente expresso dizendo que x é separado de 0 ou construtivamente diferente de 0.
Para qualquer número real x , se for contraditório que x seja igual a 0, então existe y ∈ R tal que xy = 1.

A realizabilidade modificada não justifica o princípio de Markov, mesmo que a lógica clássica seja usada na metateoria: não há diretor na linguagem do cálculo lambda simplesmente digitado, pois esta linguagem não é Turing-completa e os loops arbitrários não podem ser definidos lá.

O princípio fraco de Markov

O princípio de Markov fraco é uma forma mais fraca do princípio de Markov que pode ser declarado na linguagem da análise como

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

É uma declaração condicional sobre a decidibilidade da positividade de um número real.

Essa forma pode ser justificada pelos princípios de continuidade de Brouwer , enquanto a forma mais forte os contradiz. Assim, pode ser derivado do raciocínio na lógica intuicionista, alcançável e clássica, em cada caso por razões diferentes. Mas este princípio não é válido no grande sentido construtivo do Bispo.

Veja também

Análise Construtiva
Tese de Church (matemática construtiva)

Referências

Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Verlag (1973), Teorema 4.2.4 da 2ª edição.
Harvey Friedman. Funções recursivas classicamente e intuicionisticamente comprováveis. Em Scott, DS e Muller, GH Editors, Higher Set Theory, Volume 699 de Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28.
Ulrich Kohlenbach , " Sobre o princípio de Markov fraco ". Mathematical Logic Quarterly (2002), vol 48, edição S1, pp. 59–65.

links externos

Matemática construtiva (Stanford Encyclopedia of Philosophy)