Decidibilidade

Tal como acontece com o conceito de um conjunto decidível, a definição de uma teoria decidível ou sistema lógico pode ser dada tanto em termos de métodos eficazes ou em termos de funções computáveis. Estes são geralmente considerados equivalentes pela Tese de Church. De fato, a prova de que um sistema lógico ou uma teoria é indecidível usa a definição formal de computabilidade para mostrar que um determinado conjunto não é um conjunto decidível, e depois utiliza a tese de Church para mostrar que a teoria ou sistema lógico não é decidível por qualquer método eficaz (Enderton 2001, pp 206ff.).

Cada sistema lógico possui um componente sintático, que entre outras coisas determina a noção de demonstrabilidade, e um componente semântico, o qual determina a noção de validade lógica. Além disso, as fórmulas logicamente válidas de um sistema às vezes são chamadas de teoremas do sistema, especialmente no contexto da lógica de primeira ordem, em que o teorema da completude de Gödel estabelece a equivalência de consequência semântica e sintática. Em outros ramos, como na lógica linear, a relação consequência sintática pode ser usada para definir os teoremas de um sistema. Um sistema lógico é decidível se existe um método eficaz para determinar se fórmulas arbitrárias são teoremas do sistema. Por exemplo, a lógica proposicional é decidível, pois o método da tabela verdade pode ser usado para determinar se uma fórmula arbitrária proposicional é logicamente válida. Lógica de primeira ordem não é decidível; em particular, o conjunto de validações lógicas de qualquer assinatura que inclui a igualdade e pelo menos um outro predicado com dois ou mais argumentos não é decidível. Assim, sistemas lógicos estendendo lógica de primeira ordem, como de lógica de segunda ordem e teoria dos tipos, também são indecidíveis.

Uma teoria é um conjunto de fórmulas, que aqui se presume ser fechado sob consequência lógica. Ademais, a questão da decidibilidade de uma teoria é se existe um procedimento efetivo que, dada uma fórmula arbitrária na assinatura da teoria, decide se a fórmula é um membro da teoria ou não. Este problema surge naturalmente quando uma teoria é definida como o conjunto de consequências lógicas de um conjunto fixo de axiomas. Exemplos de teorias de primeira ordem decidíveis incluem a teoria de campos reais fechados, e a aritmética de Presburger, enquanto a teoria dos grupos e aritmética de Robinson são exemplos de teorias indecidíveis. Existem vários resultados sobre decidibilidade de teorias. Por exemplo, toda teoria inconsistente é decidível, já que toda fórmula na assinatura da teoria será uma consequência lógica de, e, portanto, membro, da teoria. Cada teoria completa recursivamente enumerável de primeira ordem é decidível. Uma extensão de uma teoria decidível não pode ser decidível. Por exemplo, existem teorias indecidíveis na lógica proposicional, embora o conjunto de validações (a menor teoria) seja decidível.

O método da interpretação é frequentemente usado para estabelecer indecidibilidade das teorias. Se uma teoria T essencialmente indecidível é interpretável em uma teoria consistente S, então S é também essencialmente indecidível. Isto está intimamente relacionado ao conceito de uma redução de muitos-para-um em teoria da computação.

Uma propriedade de uma teoria ou sistema lógico mais fraca do que decidibilidade é a semidecidibilidade. Dessa forma, uma teoria é semidecidível se há um método eficaz que, dada uma fórmula arbitrária, irá sempre dizer corretamente quando a fórmula está na teoria, mas pode dar tanto uma resposta negativa ou nenhuma resposta quando a fórmula não esta na teoria. Por outro lado, um sistema lógico é semidecidível se há um método eficaz para a geração de teoremas (e somente teoremas) de tal forma que cada teorema acabará por ser gerado. Logo, isso é diferente de decidibilidade, já que em um sistema semidecidível pode haver nenhum procedimento eficaz para verificar que uma fórmula não é um teorema. Toda teoria decidível ou sistema lógico é semidecidível, mas, em geral, o inverso não é verdadeiro; uma teoria é decidível se e somente se a ela e seu complemento são semi-decidíveis. Por exemplo, o conjunto V de validades lógica de primeira ordem lógica é semi-decidível, mas não decidível. Nesse caso, é porque não existe um método eficaz para determinar quando uma dada fórmula arbitrária A, se A está ou não está em V. Da mesma forma, o conjunto de consequências lógicas de qualquer conjunto recursivamente enumerável de axiomas de primeira ordem é semidecidível.

Decidibilidade não deve ser confundida com completude. Por exemplo, a teoria dos campos algebricamente fechados é decidível, porém incompleta, enquanto o conjunto de todas as declarações verdadeiras de primeira ordem sobre inteiros não negativos na linguagem com '+' e '×' é completa, mas indecidível.