La fonctionnalité est la propriété d'une sémantique formelle polyvalente selon laquelle la valeur d'une formule logique dépend exclusivement de la valeur de vérité des formules qui la composent et de la façon dont elles sont composées.. Lorsque cette propriété est vérifiée, on appelle une telle sémantique fonctionnelle ou .
En d'autres termes, dans une sémantique polyvalente avec pour ensemble de valeurs, la fonctionnalité permet de traiter chaque opération logique -aire comme une fonction de dans . Ces fonctions sont parfois appelées tables de vérité ou fonctions de vérité.
Conséquence sémantique et valeurs désignées Une propriété de désignation est une propriété qui s'hérite des prémisses vers le conséquent : si toutes les prémisses sont désignées, alors le conséquent est désigné à son tour. Ce critère de désignation peut être celui de la vérité..
Dans une sémantique fonctionnelle 𝒮, avec pour ensemble de valeurs, on définit alors un sous-ensemble de valeurs désignées, on peut ainsi définir la conséquence sémantique comme suit : pour toutes formules logiques , ..., et , les deux affirmations suivantes sont équivalentes. : que pour toute assignation de valeurs dans à chaque variable propositionnelle, soit a une valeur désignée, c'est-à-dire dans , soit il y a une des prémisses de à qui n'est pas désignée, c'est-à-dire dans , soit les deux ; que {, ..., } ⊨ , c'est-à-dire que est une conséquence de {, ..., } dans la sémantique .
Par exemple, la logique classique est équivalente à une sémantique fonctionnelle bivalente , telle que ={0;1} et ={1}. Les seules opérations logiques dans sont la conjonction (∧), la disjonction (∨) et la négation (¬).
0 1 0 0 0 1 0 1{| class="wikitable" style="text-align: center;" 0 1 0 0 1 1 1 1
| {| class="wikitable" style="text-align: center;"
! !!
! 0 | 1 |- ! 1 | 0
Nous pouvons ainsi vérifier que en vérifiant chaque assignation possible des variables propositionnelles et : Variables Prémisses Conséquent Contre-modèle ? 0 0 0 1 1 Non : la prémisse n'est pas désignée. 1 1 0 0 Non : la prémisse n'est pas désignée. 1 0 1 1 1 Non : le conséquent est désigné. 1 1 0 1 Non : le conséquent est désignée et la prémisse n'est pas désignée. Conclusion Pas de contre-modèle, la conséquence est donc valide.
De fait, la conséquence sémantique est l'analogue pour la sémantique fonctionnelle des tests d'hypothèses statistiques pour la méthode hypothético-déductive, en cela que l'on montre que rien ne permet de rejeter la règle, plutôt qu'une forme plus directe, positive ou langagière de conséquence qui consisterait à chercher ce qui permettrait de prouver la règle à l'instar de la conséquence syntaxique.
Correction et complétude
En s'assurant qu'une sémantique fonctionnelle 𝒮 est soumise aux mêmes règles qu'une théorie démonstrative 𝒯 donnée, 𝒮 devient une sémantique dite saine ou correcte pour 𝒯, ce qui signifie que implique à traduction près. Celles-ci peuvent être trouvées en soumettant un nombre fini de valeurs et d'opérations internes sur ces valeurs aux mêmes règles logiques que le système dont on cherche à trouver une sémantique saine, que ce soit à la main, par le biais d'un solveur de problème SAT automatique ou autre assistant de preuve.
Si la réciproque est vraie, à savoir que implique à traduction près, on dit alors que 𝒮 est une sémantique complète pour 𝒯. Une sémantique 𝒮 complète et saine pour 𝒯 fait qu'à traduction près, et décrivent la même relation de conséquence, ce sont des logiques équivalentes.
Intérêts Beaucoup de propriétés du métalangage sont difficilement obtenables par la seule théorie de la démonstration d'une logique donnée. Dans les sémantiques fonctionnelles, cependant, chaque interprétation des variables propositionnelles conduit chaque valeur à agir comme une classe d'équivalence sur les formules construites à partir desdites variables. Ainsi, lorsqu'une sémantique fonctionnelle a un nombre fini de valeurs, la plupart des propriétés de sa relation de conséquence peuvent être vérifiées en explorant un nombre fini de cas.
Sémantiques correctes
Non-trivialité, non-théorèmes, non-règles Une théorie démonstrative permet de déterminer quelles règles sont dérivables à partir des règles de base, mais plus difficilement ce qui n'est pas dérivable, c'est-à-dire les non-règles. Pour cela, on passe par des modèles sémantiques sains pour cette logique.
Une sémantique fonctionnelle 𝒮 est triviale si =, c'est-à-dire qui n'a aucune valeur non-désignée, sinon elle est non-triviale.
S'il existe une sémantique fonctionnelle non-triviale 𝒮 saine pour 𝒯, alors puisqu'on peut assigner à une valeur non-désignée grâce à la non-trivialité de 𝒮.
Plus généralement, pour toute sémantique fonctionnelle 𝒮, si et 𝒮 est saine pour 𝒯, alors à traduction près. Cela permet en particulier de déceler des non-théorèmes et des non-règles de 𝒯 à partir d'une sémantique fonctionnelle qui lui est saine.
Pour reprendre notre sémantique pour la logique classique, nous pouvons montrer ce qui conduit à la non-règle en logique classique.
Variables Prémisse Conséquent Contre-modèle ? 0 0 0 0 Non : la prémisse n'est pas désignée. 1 1 1 Non : le conséquent est désigné. 1 0 1 0 Oui : la prémisse est désignée tandis que le conséquent n'est pas désigné. Conclusion Il existe un contre-modèle, la conséquence n'est pas valide.
Inexistence de théorèmes Il est également possible de déterminer si une théorie démonstrative 𝒯 n'admet aucun théorème à partir d'une sémantique fonctionnelle 𝒮 saine pour 𝒯. Pour cela, il suffit de trouver un ensemble qui vérifient les propriétés suivantes : est un sous-ensemble non-vide de , étant donc composé uniquement de valeurs non-désignées. est un ensemble stable par toutes les opérations logiques. S'il existe des constantes logiques dans 𝒮, par exemple ⊥, celles-ci ont toute une valeur dans .
Prenons le cas de la logique . En tant que sémantique fonctionnelle, ses seules opérations logiques sont la conjonction, la disjonction et la négation, tandis que et
true both neither false true true both neither false both both both false false neither neither false neither false false false false false false{| class="wikitable" style="text-align: center;" true both neither false true true true true true both true both true both neither true true neither neither false true both neither false
| {| class="wikitable" style="text-align: center;"
! !!
! true | false |- ! both | both |- ! neither | neither |- ! false | true
Ici, notre ensemble témoin n'est autre que le singleton {neither}. En effet, neither est une valeur non-désignée, fixe par toutes les opérations logiques :
Cela permet de démontrer que la logique n'admet aucun théorème.
Paracohérence Soit 𝒯 une théorie démonstrative. On dit que 𝒯 est une logique paracohérente si elle n'admet pas le principe d'explosion, c'est-à-dire que
Pour démontrer que 𝒯 est paracohérente, il suffit de trouver une sémantique 𝒮 saine pour 𝒯 qui vérifie ces deux propriétés : 𝒮 est une sémantique non-triviale, c'est-à-dire que est non-vide. 𝒮 admet au moins une valeur , c'est-à-dire qu'il existe une valeur telle que est désignée et que est désignée aussi.
En effet, car on obtient un contre-modèle en donnant à une valeur surplus, de sorte que les deux prémisses soient désignées, et à une valeur non-désignée, de sorte que le conséquent ne soit pas désigné.
Là aussi, nous pouvons vérifier la paracohérence de à partir de ce seul critère. D'une part, cette sémantique est non-triviale, puisqu'elle admet pour valeurs non-désignées les valeurs neither et false. D'autre part, la valeur both est une valeur surplus égale à sa propre négation logique, ce qui fait que both est une valeur surplus. Les critères étant réunis, nous avons donc avec pour contre-modèles ceux qui assignent à la valeur both et à soit la valeur neither, soit la valeur false.
Propriété de partage des variables
Une logique propositionnelle pertinente 𝒯 doit, en plus de rejeter le syllogisme disjonctif, satisfaire la propriété de partage de variables : si , alors et partagent au moins une variable propositionnelle commune.
Le critère de vérification de cette propriété, à partir d'une sémantique fonctionnelle saine pour 𝒯, est détaillé dans l'article sur la logique pertinente.
Sémantiques complètes Dans une théorie démonstrative 𝒯, démontrer un séquent peut s'avérer complexe. Dans certains cas, les règles d'introduction et d'élimination permettent d'abduire les raisonnements à mobiliser au vue de la forme des formules.
Prenons l'exemple du séquent en logique intuitionniste, avec les règles d'introduction et d'élimination pour la conjonction, pour la disjonction, pour la négation (avec le syllogisme disjonctif comme règle d'élimination) et pour l'implication, ainsi que toutes les règles d'identité et règles structurelles usuelles.
Cependant, une logique n'ayant pas de telles règles rend la démonstration de séquents potentiellement plus complexe.
L'intérêt majeur d'une sémantique fonctionnelle complète pour 𝒮 est donc la réduction drastique de la complexité algorithmique et la non-nécessité de trouver une preuve syntaxique d'un séquent pour s'assurer de sa démontrabilité.
Au-delà de la fonctionnalité Tables non-déterministes Certaines sémantiques polyvalentes non-fonctionnelles ont été développées. Nous pouvons notamment citer le cas des sémantiques à tables non-déterministes, ce qui fait que les opérations logiques ne sont plus tant des fonctions que des relations. La conséquence sémantique dans ces sémantiques non-déterministes consiste à vérifier toutes les assignations de formules possibles à partir de ces lois d'assignations, en procédant par disjonction de cas. Une telle sémantique pourrait ressembler à ça :
T F T T F F F F{| class="wikitable" style="text-align: center;" T F T T T F T F
| {| class="wikitable" style="text-align: center;"
! !! T !! F
! T | T ou F || F |- ! F | T ou F || T ou F
{| class="wikitable" style="text-align: center;"
! !!
! T | F |- ! F | T ou F
On peut par exemple tester le modus ponens dans cette sémantique.
Variables Prémisses Conséquent Contre-modèle ? T T T T T Non : le conséquent est désigné.
F
Non : la prémisse n'est pas désignée, le conséquent est désigné. F F T F Non : la prémisse n'est pas désignée. F T T F T Non : la prémisse n'est pas désignée, le conséquent est désigné.
F
Non : les prémisses et ne sont pas désignées, le conséquent est désigné. F T F F Non : la prémisse n'est pas désignée.
F
Non : les prémisses et ne sont pas désignées. Conclusion Pas de contre-modèle, la conséquence est donc valide.
Non-déterminisme restreint
Dans certains cas, ces sémantiques non-déterministes utilisent des restrictions. Un exemple majeur est la sémantique trivalente non-déterministe saine et complète pour la logique intuitionniste, donné par l'ensemble de valeurs l'ensemble de valeurs désignées et pour tables non-déterministes les suivantes, puis en imposant diverses restrictions développés dans le papier dans Leme et al. (2025). :
T U F T T F F U F F F F F F F{| class="wikitable" style="text-align: center;" T U F T T T T U T F F F T F F
T U F T T F F U T U ou T U ou T F T U ou T U ou T
| {| class="wikitable" style="text-align: center;"
! !!
! T | F |- ! U | U ou T |- ! F | U ou T
Modèles structurels et algébriques Différents systèmes logiques peuvent être modélisés en tant que structures algébriques ou au moins structurels. C'est notamment le cas de la logique classique avec les algèbres de Boole, de la logique intuitionniste avec les algèbres de Heyting, de la logique pertinente avec les monoïdes de De Morgan ou encore en logique quasi-pertinente -mingle (ou ) avec les modèles de Sugihara.
Toutefois, bien que ces structures ne sont pas des sémantiques fonctionnelles à elles seules, celles-ci le deviennent généralement lorsqu'on définit ce qu'est une interprétation sémantique de formules dans ces modèles.