Sémantique catégorique des preuves-théoriques

Résumé Dans la sémantique des preuves-théoriques, la validité théorique des modèles est remplacée par la validité des preuves-théoriques. La validité des formules est définie de manière inductive à partir d'une base donnant la validité des atomes à l'aide de clauses induites dérivées des règles des preuves-théoriques. Un objectif clé est de montrer la complétude des règles de preuve sans aucune exigence de modèles formels. Établir cela pour la logique intuitionniste propositionnelle soulève des problèmes techniques et conceptuels. Nous relions la sémantique d'extension de base (complète) de la logique propositionnelle intuitionniste de Sandqvist à la théorie des preuves catégoriques dans les présheaves, en reconstruisant catégoriquement les arguments de cohérence et de complétude, démontrant ainsi la naturalité des constructions de Sandqvist. Cette naturalité inclut le traitement de la disjonction par Sandqvist, basé sur sa présentation en tant que règle d'élimination ou d'ordre supérieur. Ces constructions incarnent non seulement la validité, mais aussi certaines formes d'objets de justifications. Cette analyse est approfondie en montrant que, du point de vue de la validité, la sémantique de Sandqvist peut également être vue comme la disjonction naturelle dans une catégorie de faisceaux.