Le théorème de compacité du FOL a-t-il été formalisé dans Coq / Isabelle / etc?
15
J'ai cherché une formalisation du théorème de compacité pour FOL, mais je n'en ai pas trouvé. Quelqu'un est-il au courant d'un tel développement ou d'un travail connexe?
Avez-vous essayé de demander sur les listes de diffusion Coq ou Isabelle?
Dave Clarke
2
Je ne sais pas si cela convient à la théorie, mais voyez ceci . La complétude est là et la compacité n'en est pas loin.
Kaveh
Voir aussi l' entrée AFP pour une version en Isabelle / HOL (à partir de 2004).
Makarius
Réponses:
17
Le théorème de compacité pour la logique classique du premier ordre est une conséquence directe du théorème de complétude, et, en fait, on peut prouver directement la compacité par l'argument de style Henkin utilisé pour la complétude sans jamais mentionner de dérivation.
Le théorème de complétude pour le FOL classique par rapport aux modèles Tarski standard a été formalisé dans Mizar. Voir la série d'articles sous http://fm.mizar.org/2005-13/fm13-1.html
Je dis "presque" car il y a un point technique, prouvant la justesse d'un algorithme de tri, que je n'ai pas encore eu le temps de finir, cependant l'ingrédient principal (théorème constructif d'ultra-filtre pour les langues dénombrables) est formalisé.
On peut également considérer la complétude, et donc la compacité, pour une notion non standard de validité, et obtenir une preuve constructive complète et formalisée.
Réponses:
Le théorème de compacité pour la logique classique du premier ordre est une conséquence directe du théorème de complétude, et, en fait, on peut prouver directement la compacité par l'argument de style Henkin utilisé pour la complétude sans jamais mentionner de dérivation.
Le théorème de complétude pour le FOL classique par rapport aux modèles Tarski standard a été formalisé dans Mizar. Voir la série d'articles sous http://fm.mizar.org/2005-13/fm13-1.html
Le même théorème d'exhaustivité, mais avec une preuve constructive, a été presque formalisé par moi-même dans l'assistant de preuve Coq, voir le fichier zip sous https://sites.google.com/site/dankoilik/publications/phd-thesis
Je dis "presque" car il y a un point technique, prouvant la justesse d'un algorithme de tri, que je n'ai pas encore eu le temps de finir, cependant l'ingrédient principal (théorème constructif d'ultra-filtre pour les langues dénombrables) est formalisé.
On peut également considérer la complétude, et donc la compacité, pour une notion non standard de validité, et obtenir une preuve constructive complète et formalisée.
la source
La compacité pour le FOL a été réalisée en HOL par John Harrison, et rapportée aux TPHOLs 1998. Voir Formaliser la théorie de base du modèle de premier ordre .
la source