Theory of valuation (Q2735686)

Résumé: On montre que les logiques vérifiant les lois d'identité et de coupure infinies (logiques normales) ont une sémantique bivalente adéquate constituée par les fonctions caractéristiques des théories closes (sémantique de l'évaluation). Si de plus ces logiques sont compactes alors on peut prendre la sémantique bivalente constituée par les fonctions caractéristiques des théories saturées (sémantique de la valuation). Cette sémantique est minimale et donc comme toute théorie maximale est saturée, la sémantique constituée par les fonctions caractéristiques des théories maximales s'avère caduque si elle se différencie de la précédente. On introduit ensuite la notion de calcul, c'est une logique définie à partir des notions de règles et de démonstrations. La définition la plus simple correspond aux calculs de Hilbert. Les calculs de Hilbert sont en fait des logiques normales et réciproquement. Une définition plus complexe donne lieu aux calculs de Gentzen dont les calculs de Hilbert sont des cas particuliers. Si on considère l'ensemble des applications à valeur dans \(\{0,1\}\) respectant les règles engendrant un calcul on s'aperçoit qu'une telle sémantique (sémantique de la révaluation) est saine et même qu'elle coïncide avec la sémantique de l'évaluation dans le cas de règles de Hilbert.NEWLINENEWLINENEWLINETout ces résultats concernent des logiques dont la nature des objets n'est pas spécifiée. On définit à présent différents ensembles d'objets qui seront les domaines de logiques particulières. On présente ensuite une série de calculs correspondant à ces différents langages. De manière unitaire et progressive ou prouve les théorèmes d'adéquation en appliquant les résultats généraux de la primière partie: de la logique implicative propositionnelle classique jusqu'à la logique classique d'ordre supérieur, en passant par la logique propositionnelle quantifiée et la logique infinitaire. On s'intéresse ensuite à la question de la vérifonctionnalité: une logique vérifonctionnelle est une sous-logique d'dune version de la logique classique et un ensemble de règles engendrant un calcul vérifonctionnel est contenu dans un ensemble de règles engendrant une version de la logique classique. Pour finir on traite du problème de la décidabilité: une logique est décidable si elle l'est par la méthode des tables de vérité que est une généralisation de la méthode classique.