Sur la décidabilité de la logique du premier ordre monadique en Calcul des séquents
Barra lateral de artigos
Conteúdo do artigo principal
Resumo
Cet article présente une démonstration syntaxique de la décidabilité de la logique du premier ordre monadique (et corollairement de sa complétude pour les modèles finis). Cette démonstration est obtenue en modifiant, pour l'adapter au cas de la logique monadique, la démonstration du théorème de complétude pour la logique du premier ordre classique due à Ketonen/Schütte (dont la méthode, parfois appelée, construction d'un arbre de réfutation, décrit en fait, pour le fragment propositionnel, un algorithme de décision). Alors que dans le cas général, le traitement du quantificateur existentiel, implique la prise en considération d’une infinité de termes, dans le cas monadique, les formules peuvent être mise dans une forme canonique spécifique (H. Behmann, 1922) permettant de borner, pour la réfutation des quantificateurs existentiels, le nombre des termes devant être pris en considération. Décidabilité du cas monadique et complétude de celui-ci pour les modèles finis s'ensuivent.
---
Sobre a decidibilidade da lógica de primeira ordem monádica no cálculo dos sequentes
Neste artigo apresentamos uma prova sintática de decidibilidade para a lógica monádica de primeira ordem (e de sua completude para modelos finitos). A prova é obtida a partir de uma adaptação ao caso da lógica monádica da prova obtida por Ketonen/Schütte para a completude da lógica de primeira ordem (método de "construção da árvore de refutação", que realmente descreve, para o fragmento proposicional, um algoritmo de decisão). No caso geral (isto é, não restrito à lógica monádica), o tratamento dos quantificadores existenciais impõe uma enumeração de todos os termos da linguagem, tratamento que impede a terminação do algoritmo e, portanto, a decisão. No caso monádico, no entanto, qualquer fórmula pode ser colocada em uma forma canônica específica, um resultado devido a H. Behmann (1922), forma canônica que implica que apenas um conjunto limitado de termos deve ser levado em consideração. O tratamento dos quantificadores existenciais pode assim ser feito com um número finito de termos. A decidibilidade (e completude para modelos finitos) do caso monádico pode assim ser obtida.
---
Artigo em francês.
Detalhes do artigo
Nota de Direitos Autorais
O autor do artigo ou resenha submetido e aprovado para publicação autoriza os editores a reproduzi-lo e publicá-lo na a revista O que nos faz pensar, entendendo-se os termos "reprodução" e "publicação" conforme a licença Creative Commons Atribuição-NãoComercial 4.0 Internacional. O artigo ou resenha poderá ser acessado tanto pela rede mundial de computadores (WWW – Internet), como pela versão impressa, sendo permitidas, a título gratuito, a consulta e a reprodução do texto para uso próprio de quem a consulta. Essa autorização de publicação não tem limitação de tempo, ficando os editores da revista O que nos faz pensar responsável pela manutenção da identificação do autor do artigo.