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

Conteúdo do artigo principal

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.

Detalhes do artigo

Seção
Artigos
Biografia do Autor

Jean-Baptiste Joinet, Université Jean Moulin, Lyon 3

Professor da Université Jean Moulin (Lyon 3). Professor convidado do Instituto de Filosofia e Lógica da Linguagem do Departamento de Filosofia da PUC-Rio e professor visitante do exterior na cadeira internacional do Ministério do Ensino Superior (Bosista Capes-Brasil) de março a setembro de 2014. Action Capes-Cofecub Sh-873-17. Programme Beyond-Logic (ANR-DFG).