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.
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:
( ∀ ∀ --> n ( P ( n ) ∨ ∨ --> ¬ ¬ --> P ( n ) ) ) ∧ ∧ --> ( ¬ ¬ --> ∀ ∀ --> n ¬ ¬ --> P ( n ) ) → → --> ( ∃ ∃ --> n P ( n ) ) . {\displaystyle (\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:
f {\displaystyle f} sendo uma função computável sobre os números naturais.
Na linguagem da análise real, o princípio é equivalente aos seguintes:
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 ) , … … --> {\displaystyle P(0),P(1),P(2),\dots } é verdade. Porque P {\displaystyle 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 {\displaystyle 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.
A regra de Markov é a formulação do princípio de Markov como uma regra. Ela declara que ∃ ∃ --> n P ( n ) {\displaystyle \exists n\;P(n)} é derivável logo que ¬ ¬ --> ¬ ¬ --> ∃ ∃ --> n P ( n ) {\displaystyle \neg \neg \exists n\;P(n)} seja recursivo para P {\displaystyle 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[1], usando a Tradução de Friedman.
Uma forma fraca do princípio de Markov pode ser expressa em linguagem de análise como:
∀ ∀ --> x ∈ ∈ --> R ( ∀ ∀ --> y ∈ ∈ --> R ¬ ¬ --> ¬ ¬ --> ( 0 < y ) ∨ ∨ --> ¬ ¬ --> ¬ ¬ --> ( y < x ) ) → → --> 0 < x . {\displaystyle \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.[2]
Lokasi Pengunjung: 3.145.110.107