Sur la décidabilité de la logique du premier ordre monadique en Calcul des séquents

##plugins.themes.bootstrap3.article.main##

Jean-Baptiste Joinet

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.

##plugins.themes.bootstrap3.article.details##

Como Citar
JOINET, Jean-Baptiste. Sur la décidabilité de la logique du premier ordre monadique en Calcul des séquents. O que nos faz pensar, [S.l.], v. 25, n. 39, p. 55-69, dec. 2016. ISSN 0104-6675. Disponível em: <http://oquenosfazpensar.fil.puc-rio.br/index.php/oqnfp/article/view/515>. Acesso em: 19 nov. 2017.
Seção
Artigos