# Problema indecidível

Na teoria da computação e na teoria da complexidade computacional, um problema indecidível é um problema de decisão em que é impossível construir um algoritmo que sempre responde corretamente sim ou não.
Um problema de decisão é qualquer questão arbitrária de sim-ou-não sobre um conjunto infinito de entradas. Por causa disto, é comum definir o problema de decisão de maneira equivalente como: o conjunto de entradas para o qual o problema retorna sim. Estas entradas podem ser números naturais, mas também podem ser outros valores de outros tipos, como cadeias de uma linguagem formal. Usando alguma codificação, tal como uma numeração de Gödel, as cadeias podem ser codificadas como números naturais. Para manter a definição de formalidade simples, ela é colocada em termos de subconjuntos dos números naturais.
Formalmente, um problema de decisão é um subconjunto dos números naturais. O problema correspondente de maneira informal é o de se decidir se um dado número está no conjunto. Um problema de decisão A é chamado decidível ou efetivamente solúvel se A é um conjunto recursivo. Um problema é chamado parcialmente decidível, semidecidível, solúvel, ou provável se A é um conjunto recursivamente enumerável. Problemas parcialmente decidíveis e outros problemas que não são decidíveis são chamados indecidíveis.

## O problema indecidível na teoria da computabilidade

Na teoria da computabilidade, o problema da parada é um problema de decisão que pode ser estabelecido como:
    Dada a descrição de um programa e uma entrada finita, decida se um programa termina de executar ou se ele executará para sempre.
Alan Turing provou em 1936 que um algoritmo genérico executando sobre uma máquina de Turing que resolve o problema da parada para todos os pares de entrada do programa possíveis necessariamente não pode existir. Consequentemente, o problema da parada é indecidível para máquinas de Turing.

## Relação com o teorema da incompletude de Gödel

Os conceitos levantados pelo teorema da incompletude de Gödel são muito similares com aqueles levantados pelo problema da parada, e as provas também são bastante semelhantes. De fato, uma forma mais fraca do primeiro teorema da incompletude é uma simples consequência da indecidibilidade do problema da parada. Esta forma mais fraca difere da definição padrão do teorema da incompletude definindo que uma axiotimização completa, consistente e correta de todas as definições sobre números naturais é inalcançável. A parte "correta" é a mais fraca: significa que nós queremos que o sistema axiomático em questão demonstre apenas sentenças verdadeiras sobre números naturais. É importante observar que a definição da forma padrão do primeiro teorema da incompletude de Gödel é completamente distinta da questão de verdade, mas somente diz respeito à questão de saber se ele pode ser provado.
A forma mais fraca do teorema pode ser provada a partir da indecidibilidade do problema da parada como a seguir. Assuma que nós temos uma axiomatização consistente e completa de todas as sentenças verdadeiras da lógica de primeira ordem sobre números naturais. Então nós podemos construir um algoritmo que enumera todas essas sentenças. Isto significa que existe um algoritmo N(n) o qual dado um número natural n, ele computa uma sentença da lógica de primeira ordem sobre números naturais de tal forma que, para todas as sentenças que são verdadeiras, existe pelo menos um n tal que N(n) gera aquela sentença.
Agora suponha que queremos decidir se o algoritmo com representação a para sobre a entrada i. Nós sabemos que esta sentença pode ser expressa por uma sentença da lógica de primeira ordem, por exemplo H(a, i). Como a axiomatização é completa, deduzimos que ou existe um n tal que N(n) = H(a, i) ou existe um n' tal que N(n') = ¬ H(a, i). Então, se iterarmos sobre todos os n até que achemos um H(a, i) ou a sua negação, nós sempre iremos parar. Isto significa que nós temos um algoritmo que decide o problema da parada. Como nós sabemos que não pode existir tal algoritmo, chegamos à conclusão de que a suposição que existe uma axiomatização consistente e complexa de todas as sentenças verdadeiras da lógica de primeira ordem sobre números naturais deve ser falsa.

## Exemplos de problemas indecidíveis

Problemas indecidíveis podem estar relacionados a diferentes tópicos, tais como lógica, máquinas abstratas ou topologia. Observe que, como existem incontáveis problemas indecidíveis, qualquer lista é, necessariamente, incompleta.

## Exemplos de sentenças indecidíveis

Existem dois diferentes sentidos para a palavra "indecidível" no uso contemporâneo. O primeiro deles é o sentido usado na relação para os teoremas de Gödel, que é uma sentença não sendo nem provável nem refutável em um sistema dedutivo específico. O segundo sentido é usado na relação em teoria da computabilidade e se aplica não somente a sentenças, como também a problemas de decisão, que são conjuntos contáveis infinitos de questões, cada uma requerendo uma resposta sim ou não. Tal problema é dito indecidível se não existe uma função computável que responde corretamente a cada questão do conjunto de problemas. A conexão entre estes dois é que se um problema de decisão é indecidível (no sentido de recursão teórica), então não existe um sistema formal consistente e efetivo que prova para toda questão A no problema se "a resposta para A é sim" ou "a resposta para A é não".
Por causa dos dois significados da palavra indecidível, o termo independência é, algumas vezes, usado em vez de indecidível para o sentido "nem provável nem refutável". Entretanto, o uso de "independente" também é ambíguo. Pode significar somente "não provável", deixando em aberto se uma declaração independente pode ser refutada.
A indecidibilidade de uma sentença em um sistema dedutivo em particular, por si só, não resolve a questão do valor de verdade de uma sentença ser bem definida ou se pode ser determinada por outros meios. A indecidibilidade apenas implica que o sistema dedutivo em particular sendo considerado não prova a veracidade ou a falsidade da sentença. Se existem as então chamadas sentenças "absolutamente indecidíveis", cujo valor de verdade nunca pode ser conhecido ou são mal especificados, é um ponto controverso entre várias escolas filosóficas.
Um dos primeiros problemas suspeitos de ser indecidível, no segundo sentido do termo, foi o problema da palavra para grupos, primeiramente colocado por Max Dehn em 1911, que perguntou se existe um grupo para o qual não existe algoritmo que determine se duas palavras são equivalentes. Este se mostrou ser o caso em 1952.
O trabalho combinado de Gödel e Paul Cohen deu dois exemplos concretos de sentenças indecidíveis (no primeiro sentido do termo): a hipótese do continuum não pode ser nem provada nem refutada em ZFC (a axiomatização padrão da teoria dos conjuntos, e o axioma da escolha não pode ser nem provada nem refutada na ZF (que é composto por todos os axiomas do ZFC exceto o axioma da escolha). Estes resultados não precisaram do teorema da incompletude. Gödel provou em 1940 que nenhuma destas sentenças podia ser desmentida na teoria dos conjuntos de ZF ou ZFC. Na década de 1960, Cohen provou que nenhuma delas é provável a partir do ZF, e a hipótese do continuum não pode ser provada a partir do ZFC.
Em 1970, o matemático soviético Yuri Matiyasevich mostrou que o décimo problema de Hilbert, proposto em 1900 como um desafio para os matemáticos do próximo século, não poderia ser resolvido. O desafio de Hilbert procurava um algoritmo que encontrasse todas as soluções de uma equação diofantina. Uma equação diofantina é um caso mais geral do último teorema de Fermat; nós procuramos as raízes inteiras de um polinômio com qualquer número de variáveis com coeficientes inteiros. Desde que nós tenhamos somente uma equação, mas n variáveis, infinitas soluções existem (e são fáceis de encontrar) no plano complexo; o problema se torna difícil (impossível) restringindo as soluções somente para valores inteiros. Matiyasevich mostrou que este problema é insolúvel mapeando uma equação diofantina para um conjunto recursivamente enumerável e invocando o teorema da incompletude de Gödel.
Em 1936, Alan Turing provou que o problema da parada — a questão de se definir se uma máquina de Turing para sobre um dado programa — é indecidível, no segundo sentido do termo. Este resultado foi posteriormente generalizado pelo teorema de Rice.
Em 1973, o problema de Whitehead na teoria dos grupos se mostrou indecidível, no primeiro sentido do termo, na teoria dos conjuntos padrão.
Em 1977, Paris e Harrington provaram que o princípio de Paris-Harrington, uma versão do teorema de Ramsey, é indecidível na axiomatização da aritmética dada pelos axiomas de Peano, mas podem ser provadas como verdadeiras em um sistema maior da aritmética de segunda ordem.
O teorema da árvore de Kruskal, que tem aplicações na ciência da computação, também é indecidível a partir dos axiomas de Peano, mas é provável na teoria dos conjuntos. De fato, o teorema da árvore de Kruskal (ou sua forma finita) é indecidível em um sistema muito mais forte que codifica os princípios aceitáveis com base em uma filosofia da matemática chamada predicativismo.
O teorema de Goodstein é uma sentença sobre a teoria de Ramsey dos números naturais que Kirby e Paris mostraram ser indecidíveis na aritmética de Peano.
Gregory Chaitin produziu sentenças indecidíveis na teoria da informação algorítmica e provou outro teorema da incompletude neste cenário. O teorema de Chaitin declara que para qualquer teoria que possa representar uma aritmética suficiente, existe um limite superior c tal que nenhum número específico pode ser provado nesta teoria que tenha uma complexidade de Kolmogorov maior do que c. Enquanto o teorema de Gödel está relacionado com o paradoxo do mentiroso, o resultado de Chaitin está relacionado com o paradoxo de Berry.
Douglas Hofstadter deu uma prova alternativa notável da incompletude, inspirada por Gödel, em seu livro Gödel, Escher, Bach.
Em 2006, os pesquisadores Kurtz e Simon, baseando-se em trabalhos anteriores de J.H. Conway na década de 1970s, provaram que uma generalização natural do problema de Collatz é indecidível.