Les logiques : notes en vrac

Le dire ainsi serait peut‑être plus correcte et plus précis : la notion de quantité est substituée par un jugement sur une condition d’un effet.

Précisions sur la notion de jugement.

La notion de jugement a plusieurs été mentionnée sans l’avoir assez précisé. Ce manque de précision a dut la faire mal utiliser deux ou trois fois. Ce n’est pas trop grave, comme les jugements ont juste été mentionnés sans jamais être utilisés.

D’après le CNRTL, jugement et assertion semblent synonymes : « décision mentale par laquelle le contenu d'une assertion est posé à titre de vérité » en parlant de jugement et « proposition, de forme affirmative ou négative, qui énonce un jugement et que l'on soutient comme vraie absolument  » en parlant d’assertion.

Une manière erronée d’en parler, a été de l’avoir confondu avec un opérateur. Les notations « not A » et « A false » ont au moins une fois été utilisées comme synonymes, même si c’est « not A » qui a été utilisée dans les exemples, d’une manière correcte. Le problème est que comme « not A » est un mode de résolution des variables de A de manière à ce que A ne soit pas vérifié, dire que c’est équivalent à « A false », équivaut à dire que le jugement est biaisé ou qu’il se permet d’arranger les choses de manière à ce que le jugement puisse être posé tel qu’écrit. Ce n’est pas ce qu’on comprend spontanément, en parlant de jugement, le mot sous‑entend qu’un jugement se fait sur la base de constats.

Mais le jugement a un sens plus fort qu’un constat, il affirme. Alors dans « A true », on ne fait pas que constater que A est vérifié, on pose que A doit toujours l’être, et réciproquement pour « A false ». Se pose alors la question du contexte. Si « A true » apparaît dans le corps d’une règle, faut‑il le comprendre dans le contexte d’entrée de la règle ou dans le contexte où tous les termes sont vérifiés ? Le comprendre dans le contexte ou tous les termes sont vérifiés seraient plus cohérent, parce qu’aurait le même sens, quelque soit le sens de la propagation des variables. Mais se pose un autre problème. Dans ce cas, « A false » dans le corps d’une règle, n’a aucune pertinence, car si le terme n’est pas vérifié, la règle non‑plus et le jugement ne peut être vérifié que si la règle ne peut jamais l’être. Il reste alors des choix à faire avant de poser une définition du jugement tel qu’il sera utilisé ici.

À la suite du message précédent, sans encore y répondre. Quand il est dit que les définitions varient, elles varient déjà entre la logique et la philosophie. Les définitions philosophiques, comme celle de l’encyclopédie Universalis, tiennent les proposition pour des jugements ou des assertions, tandis la page liée plus loin, souligne que c’est une confusion à ne pas faire, posant que « P true » est un jugement, mais pas P tout‑court : judgment (ncatlab.org).

Peut‑être que parler d’appréciation ou de qualification, conviendrait mieux, parler de jugement étant connoté. Parler de qualification est aussi connoté en informatique, mais la confusion est improbable : en informatique on parle de qualified name, pour parler d’un nom complet encombrant, une identité globale, par opposition à un nom court moins encombrant, une identité locale correspondant à une identité globale. Même avec le même mot, les deux sens sont tellement éloignés que la confusion est peu probable.

Ce ne sont pour le moment que des remarques.

— Édit : deux erreurs dans ce message, sont corrigées dans le message qui le suit. —

Sur les hypothèses, des notes et petits rappels. Ces notes vont peut‑être servir plus tard.

La notation {r A} correspond à (r A) posé en hypothèse, en se rappelant que ce qui fait vraiment une hypothèse, est le status des variables. Dans une hypothèse, elles sont généralisées et gelées ; elles doivent être gelées, car elles sont généralisées et les deux mots sont synonymes dans ce contexte. Un terme entièrement constant ne contenant pas de variables, {c} devrait être équivalent à (c). Dans la conjonction {r1 A B} & (r2 A) & (r2 B), A et B étant explicitement gelées, si la conjonction est vérifiée (non‑valable dans le cas contraire), elle devrait être équivalente à {r1 A B} & {r2 A} & {r2 B}, mais {r1 A B} & (r2 B C) ne peut pas être tenue pour équivalente à {r1 A B} & {r2 B C}, même si la conjonction est vérifiée, la variable C n’étant pas certainement gelée. Rien n’a jamais été prévu pour par exemple passer de {c} à (c) ou réciproquement. Une variable peut être gelée sans l’être explicitement, par exemple par la liaison d’une variable libre à une variable gelée, ailleurs, sans qu’une hypothèse n’apparaisse textuellement, par exemple si cette variable est passée par la tête d’une règle. L’inspection des variables après une vérification ou une résolution, permet de connaitre leur status, gelée ou pas. La résolution ne résous pas les variables gelées, sinon elle ne préserverait pas le sens, mais elle peut vérifier des termes en contenant, par exemple en les vérifiant par des hypothèses disponibles, mais pas seulement. Une variable non‑gelée apparaissant dans un terme contenant une variable gelée, peut malgré tout être résolue.

Compléments au message précédent et correction de deux erreurs.

Il faut bien écrire {(r A)} et non‑pas {r A}. C’est important, sinon (c) et c, se confondent une fois posés en hypothèse, chacun des deux devenant le même {c}, alors que c et (c) ne sont pas les mêmes termes.

{c} ne peut pas être équivalent à c, au moins parce que c peut avoir plusieurs cas. Même sans variables, une hypothèse peut être une abstraction de plusieurs cas. Ceci est modulo une précision ajoutée plus loin.

Même si les variables gelées font les hypothèses telles qu’elles sont, il y a plus. D’abord on ne gèle pas des variables pour faire une hypothèse, on pose une hypothèse, ce qui gèle les variables. Si on veut geler des variables, le seul moyen est de poser une hypothèse. Une hypothèse est posée d’abord, ses variables gelées ensuite en conséquence. Un second cas d’apparition d’une hypothèse, est cependant envisagé juste après.

Il faudrait distinguer les hypothèses posées, déjà vues, et les hypothèses générées, une distinction peut‑être à ajouter, mais une idée encore vague. Dans le message précédent il est dit que si la conjonction {(r1 A)} & (r2 A) est vérifiée, alors cette conjonction est équivalente à {(r1 A)} & {(r2 A)}. L’hypothèse {(r1 A)} est supposée posée et devoir être démontrée possible à moins qu’elle ne le soit déjà et que alors ses cas sont connus. Dans le cas d’une preuve ultérieure, elle ne peut pas être ouverte, dans le cas d’une preuve antérieure, elle peut être ouverte. Si la première conjonction est prouvée, le terme (r2 A) est une généralité, une propriété héritée de sa variable. Il peut être considéré comme une hypothèse générée, différente d’une hypothèse posée, parce que sa possibilité est prouvée en même temps. Une question à se poser, est ce qu’il en serait de ses cas. De la même manière et avec la même question en suspend, il serait envisageable de passer de c à {c}, mais pas l’inverse ; ce qui le justifierait, c’est qu’un terme constant est gelé par nature.

Il faudrait distinguer généralité et hypothèse. C’est le paragraphe précédent qui l’inspire. Une hypothèse est une généralité et l’est explicitement, mais une généralité n’est pas toujours une hypothèse et une généralité peut être implicite. Il faudrait prévoir un mécanisme de passage d’une généralité à une hypothèse.

Étant donné (r A B) où A est gelée, il pourrait être utile de permettre de substituer ce terme par l’hypothèse correspondante, suite à quoi B serait aussi gelée. L’idée est de permettre d’ouvrir {(r A B)}, ce qui serait utile, parce que pour le moment au moins, aucun mécanisme n’est prévu pour discriminer sur les éventuels cas de A dans (r A B), quand encore ce serait possible indépendamment de B, ce qui n’est pas le cas général.

La raison de revenir sur les hypothèses ne sera expliquée que plus tard, à condition que la raison ne s‘avère pas être une impasse. Quoiqu’il en soit, ce retour n’est pas sans intérêt en lui‑même.

D’autres compléments, toujours à la suite.

Vers fin‑Novembre 2020, avaient été rapportés deux exemples de démonstrations sous hypothèses, mais sans dire comment la conclusion de ces démonstration étaient utilisables.

Sans rappeler les règles concernées, ces deux preuves avaient été faites :

(int Z) : {(int-z Z)}.
(nat-lt N (s (s N))) : {(nat N)}.

L’utilisation prévue est que si on a prouvé un terme (int-z X), alors sa mise en correspondance avec {(int-z Z)}, permet de prouver le terme (int X), instantanément. Que la tête de ce qui ressemble à une règle et en est bien une dans son genre, ressemble à un terme ordinaire, n’en fait pas pour autant une règle utilisable par résolution, ce qui est mécaniquement impossible, comme la condition est un terme gelé. Ces explications avait été omises.

Avant de passer à la suite, qui se place dans le contexte avant ce paragraphe, ce qui avait été omis aussi, c’est que ce type de formule pourrait apparaître dans la liste des règles, avec les règles ordinaires, et de plus, sans nécessairement être utilisées pour prouver des termes, même si cette possibilité resterait toujours ouverte, dès qu’une telle règle serait présente. L’autre usage que pour vérifier des termes, serait d’être la preuve de propriétés de règles, précédemment mentionnée, mais avec des limites qui seront abordées le moment venu. La règle vaudrait le seule fait d’être là et d’être vérifiée, même en étant jamais appliquée.

Retour dans le contexte d’avant le paragraphe précédent. Il y a autant de différence entre ces règles et les autres que, en se replaçant dans ce qui été précédemment introduit, entre une règle mentionnée par la couche du dessus et la même règle mentionnée par sa propre couche. Elles fonctionnent en bonne partie, comme une règle d’une première couche quand elle est mentionnée par une règle d’une seconde couche, et cela, même si elle sont mentionnée depuis leur propre couche. Il faudrait alors penser à déterminer comment elles se comportent si elles sont mentionnées depuis la couche du dessus. L’approche de la question nécessite un pas trop long exposé des situations.

D’abord un rappel qui est aussi une reformulation. Si dans une couche #1 on a une règle « A : B. », que dans une couche #2 on a un terme littéral A et un terme littéral B, alors le terme A devient un terme vérifié et se voit attribué du sens d’après le terme littéral ou vérifié B, le terme B pouvant être lui‑même sujet au même processus. Un terme littéral est à comprendre comme un terme non‑vérifié, ce qui ne signifie pas qu’on puisse vérifier n’importe quoi, la conclusion du processus peut d’ailleurs laisser des termes non‑vérifiés, il faut alors juger ou pas de l’adéquation de ce résultat, ou le processus peut aussi s’arrêter sur une contradiction. On ne peut pas aboutir à n’importe quoi, parce que les termes font tous partie d’une conjonction et sont donc dans un même contexte, qui garde la trace de tout ce qui a été vérifié et avec quoi il faudra être en accord. Un terme utilisé pour vérifier un autre terme, pourra aboutir à une contradiction s’il est incorrecte. Pour ce qui est de l’intention, les règles de la couche #1 définissent un langage et les conjonctions de la couche #2, sont un propos dans ce langage.

Maintenant, la nouveauté a aborder. Si dans une couche #1 on a une règle « C : {D}. », alors si dans cette couche #1 on a un terme vérifié E et qu’il correspond à D, alors on obtient un terme vérifié C. Mais si dans une couche #2 on a un terme littéral E correspondant à D, est‑ce suffisant pour vérifier un terme C dans la couche #2 ? Dans ce cas, la règle « C : {D}. » aurait presque le même comportement depuis sa propre couche et depuis une couche au dessus et le même comportement que n’importe quelles autres règles d’une couche #1, depuis une couche #2 d’où elle serait indistinguable. Il a été dit « presque » à propos du premier point, parce que le terme E mis en correspondance, pourrait être non‑vérifié, alors que depuis la première couche, le terme doit être vérifié avant d’être appliqué à la règle. Mais après tout, les règles ordinaires aussi, sont sensés ne produire que des termes vérifiés quand elles fonctionnent en résolution, et pourtant, elles acceptent des termes non‑vérifiés depuis la couche #2, et sans ça, les règles mutuellement dépendantes pourtant cohérentes, ne seraient pas vérifiables. Le contexte se charge de la validation de l’accord de ces termes entre eux, et d’ailleurs la mise en correspondance par l’unification, est déjà une première validation même sur un terme littéral. Il pourrait en être de même avec les règles de la forme « C : {D}. ». Ceci dit, il serait peut‑être aussi possible d’envisager qu’elles ne s’appliquent qu’à des termes vérifiés par d’autres règles. Par exemple E de la couche #2 devrait d’abord être vérifié par une règle de la couche #1, seulement après quoi E vérifié, pourrait être utilisé pour vérifié un terme C. Mais qu’est‑ce qui justifierait ce détour et ne pourrait‑il pas devenir un problème pour d’éventuelles dépendances mutuelles ?

Il faudrait distinguer terme produit et terme vérifié.

Plutôt distinguer trois états d’un terme : littéral, hypothétique et vérifié. Ces états seraient distincts des types d’interprétation d’un terme, sans en être indépendants. Cette notion d’état semble nécessaire pour définir la sémantique des couches superposées précédemment décrites.

Concernant ces couches superposées, des précisions sont encore à apporter. Ce qu’il en a été dit manque encore trop de précisions.

À une liste précédemment posée, des différentes interprétations d’un terme, il faut aussi ajouter, le terme interprété comme un fait ou une chose posée.

Sur les hypothèses, des idées semblant assez certaines, mais peut‑être pas correctement dites et nécessitant des clarifications sur leurs conséquences.

À chaque règle « A : B. » correspond une règle « A : {B}. » implicite. Elle peut être implicite, parce que même si comme toutes règles ayant une hypothèse comme condition, elle doit être prouvée, sa preuve existe déjà, c’est « A : B. »

Une banalité préalable : dans « A : {B}. », {B} est une généralité à laquelle on peut substituer un cas particulier et concret de {B}, pour obtenir un A spécifique. Idée de voir un terme partiellement résolu ou vérifié, comme une sorte d’hypothèse : un terme partiellement déterminé, a le même rapport aux termes plus déterminés qui en dérivent, que {B} par rapport à un cas particulier de {B}. Et aussi, la forme entièrement déterminée du terme, peut–elle être vue comme la preuve ultérieure d’une hypothèse ?

A & B & C, par exemple, est un cas particulier de A & B, autant qu’un cas particulier de B & C, autant qu’un cas particulier de A & C. C’est la reformulation d’une banalité, qui fait remarquer un lien avec le paragraphe précédent.

— Édit pour ajout : pendant la vérification ou la résolution d’un terme qui est une interprétation, on est sous l’hypothèse de ce terme. Voir le message suivant pour un exemple de cas d’utilisation. —

Rappel en marge : une hypothèse peut être utilisée sans preuve préalable, une preuve ultérieure à son utilisation est autant valable qu’une preuve qui lui est antérieure (la seule différence entre les deux est dans la disponibilité de la couverture des cas).