Decidibilidade

Em lógica, o termo decidível se refere a um problema de decisão, ou seja, a questão da existência de um método efetivo para determinar a pertinência em um conjunto de fórmulas. Sistemas lógicos, tais como a lógica proposicional, são decidíveis se a pertinência em seu conjunto de fórmulas logicamente válido pode ser efetivamente determinado. Uma teoria (conjunto de fórmulas fechada sob a consequência lógica) em um sistema lógico fixo é decidível se existe um algoritmo eficiente para determinar se fórmulas arbitrárias pertencem a ela. Muitos problemas importantes são indecidíveis.

Relação com computabilidade

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

Decidibilidade de um sistema lógico

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.

No entanto, as validações do cálculo monádico de predicados com identidade são decidíveis. Esse sistema é lógica de primeira ordem restrito a assinaturas que não têm símbolos de função e cujos outros símbolos de relação (com exceção da igualdade) não pode ter mais de um argumento.

Alguns sistemas lógicos não são adequadamente representados apenas pelo conjunto de teoremas. Por exemplo, a lógica de Kleene. Nesses casos, definições alternativas de decidibilidade são muitas vezes utilizadas, as quais pedem um método eficaz para determinar algo mais geral do que apenas a validade de fórmulas, por exemplo, validade de sequentes, ou a relação de consequência {(Г, A) | Г ⊧ a} da lógica.

Decidibilidade de uma teoria

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.

Uma teoria consistente que tem a propriedade de que cada extensão consistente é indecidível é dito ser essencialmente indecidível. Na verdade, toda extensão consistente será essencialmente indecidível. A teoria dos campos é indecidível, mas não essencialmente indecidível. Aritmética de Robinson é conhecida por ser essencialmente indecidível, e, portanto, cada teoria consistente que inclui ou a interpreta aritmética também é (essencialmente) indecidível.

Algumas teorias decidíveis

O conjunto de primeira ordem de validações lógicas na assinatura com apenas igualdade, instituído por Leopold Löwenheim em 1915.
O conjunto de primeira ordem de validações lógicas em uma assinatura com a igualdade e uma função unária, instituído pela Ehrenfeucht em 1959.
A teoria de primeira ordem dos números inteiros na assinatura com igualdade e adição, também chamada de aritmética de Presburger. Sua completude foi estabelecida por Mojżesz Presburger em 1929.
A teoria de primeira ordem de álgebras booleanas, criada por Alfred Tarski em 1949.
A teoria de primeira ordem dos campos algebricamente fechados sob uma dada propriedade, estabelecida por Tarski em 1949.
A teoria de primeira ordem dos realmente fechados campos ordenados, estabelecida por Tarski em 1949.
A teoria de primeira ordem da geometria euclidiana, instituída por Tarski em 1949.
A teoria de primeira ordem da geometria hiperbólica, instituída por Schwabhäuser em 1959.

Algumas teorias indecidíveis

O conjunto de validades lógicas em qualquer assinatura de primeira ordem com igualdade e ou um símbolo de relação de aridade não menor do que 2, ou dois símbolos de função unária, ou um símbolo de função de aridade não menor que 2, instituído por Trakhtenbrot em 1953.
A teoria de primeira ordem dos números naturais com a adição, multiplicação e igualdade, estabelecida por Tarski e Mostowski Andrzej em 1949.
A teoria de primeira ordem dos números racionais com a adição, multiplicação e igualdade, estabelecido por Julia Robinson em 1949.
A teoria de primeira ordem dos grupos, instituída por Mal'cev em 1961.
A aritmética de Peano é essencialmente indecidí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.

Semidecidibilidade

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.

Relação com completude

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.

Ver também

Referências

Barwise, Jon (1982), "Introduction to first-order logic", in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
Cantone, D., E. G. Omodeo and A. Policriti, "Set Theory for Computing. From Decision Procedures to Logic Programming with Sets," Monographs in Computer Science, Springer, 2001.
Chagrov, Alexander; Zakharyaschev, Michael (1997), Modal logic, Oxford Logic Guides, 35, The Clarendon Press Oxford University Press, ISBN 978-0-19-853779-3, MR1464942
Davis, Martin (1958), Computability and Unsolvability, McGraw-Hill Book Company, Inc, New York
Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
Keisler, H. J. (1982), "Fundamentals of model theory", in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
Monk, J. Donald (1976), Mathematical Logic, Berlin, New York: Springer-Verlag