Les logiques : notes en vrac

En lisant la négation comme ayant un sens dépendant du sens du terme auquel elle s’applique, en considérant que non T n’est pas un terme, que c’est T qui est un terme, que l’impossibilité peut être constatée seulement pour un terme dans un contexte, le casse tête de la négation disparaît et il est possible de réintroduire avec bien de moins de confusion qu’auparavant, certaines précédentes idées de distinctions entre les termes pour eux‑mêmes, comme l’idée que certains termes se lisent comme « les solutions tel que », implicitement dans un nouveau contexte ou « tel‑quel dans ce contexte », avec des jugements s’y appliquant, comme « pas de solution trouvée le rendant impossible », « ne peut pas être impossible », « impossible sans besoin de solution », « rendu impossible par cette solution », « non vérifié tel‑quel sans recherche de solution », la négation étant une interprétation de ces jugements. Restant à organiser, mais plus clair qu’auparavant, comme il s’agit de propriété des termes, non T n’est pas un terme, seulement T l’étant. Ces jugement étant posés (ce qui resterait à faire proprement), la négation étant une interprétation de ces jugements, elle pourrait recevoir une signification plus concrète, selon les termes, conformément à l’idée précédente.

Pour changer du casse‑tête qui s’entête à durer, un retour sur la question des termes cycliques.

À première vu et rapidement, il pourrait sembler surprenant que des règles puissent décrire comme correctes des termes qui ne peuvent pas être écrits. Ça s’explique par une différence entre les termes apparaissant dans les règles et les termes écrits pour être vérifiés ou pas : les termes des règles contiennent des variables. Ces variables font que les règles peuvent décrire un nombre nombre de termes effectifs, qu’elles‑mêmes ne contiennent elles‑mêmes de termes abstraits. Sans les variable, les règles ne pourraient décrire qu’un ensemble fini de termes, qu’elles listeraient exhaustivement. Seulement, la présence de ces variables ne fait pas que permettre de décrire une infinité de termes possibles avec un nombre fini de termes abstraits, ces variables permettent aussi d’écrire des termes qu’il n’est pas possible d’écrire avec la même syntaxe mais sans variables. Les termes cyclique en sont un exemple.

Une idée de notation a été proposée pour permettre d’écrire les termes cycliques. Mais cela est‑il suffisant ? Une question laissée en suspend à ce moment là, suggérait déjà que non : il est possible d’imaginer un cycle dans un cycle et l’idée de notation proposée ne le prévoyait pas. Elle pourrait être étendue en prévoyant le cas, sous réserve qu’il s’agisse strictement de cycles inclus dans un cycle. Mais serait‑ce suffisant ? Intuitivement, non, parce que la différence entre les termes écrits dans les règles et les termes écrits pour être vérifiés, resterait toujours : les premiers auraient des variables, toujours pas les seconds et cette différence aurait toujours la même conséquence. La solution la plus certaines, pour que les termes potentiellement vérifiables puissent tous être écrits, serait que les termes puissent être écrits avec des variables et il n’y aurait alors plus de différence d’expressivité entre les deux (il faudrait le démontrer quand‑même), concernant l’écriture des termes au moins. L’idée de notation pour représenter un terme cyclique par un symbole représentant le point d’entrée et un symbole représentant le point de « sortie » revenant à l’entrée, pourrait être améliorée en ayant une notation pour nommer ces points d’entrée et de « sortie », chaque entrée nommée devant correspondre à une sortie nommée. Ce serait une manière d’introduire des variables dans les termes (des variables jamais libres, jamais indéfinies), assurant que tous les termes vérifiables par des règles, puissent effectivement être écrits.

Mais l’idée d’introduire des variables dans les termes pour permettre d’écrire tous les graphes et les cycles que des règles peuvent valider, cette idée d’introduire des variables dans les termes, pourrait être intimidante à cause de la complexité supplémentaire qui viendrait peut‑être avec avec.

L’idée de se contenter d’une notation plus simple pour représenter des cycles simples, semble alors intéressante. Mais il faut considérer alors qu’il resterait toujours possible d’écrire des règles vérifiant des termes qu’il serait impossible de vérifier, faute de pouvoir les écrire.

L’idée de terme contenant des variables, garantissant de pouvoir écrire tous les termes possiblement vérifiables, même si elle est intimidante, n’est pas à exclure. Il faudrait juste ne pas s’y précipiter, surtout si elle n’est pas une nécessité pratique, une raison théorique n’étant pas une raison pratique suffisante si on a pas de raison simplement pratique de le faire.

Complément au message précédent.

Plutôt que des noms de variables, les termes complexes avec des cycles et d’autres relations internes, pourraient au lieu de nommer les points connectés entre eux, les numéroter, en utilisant des numéros en partant de 1 et en suivant. Ça permettrait d’avoir une représentation potentiellement plus canonique.

Oops, c’était une erreur : le corps d’une règle peut contenir des variables n’apparaissant pas dans la tête de la règle et ne pouvant pas être substituées immédiatement à un terme constant. Ces variables ne peuvent être fixées que par la résolution du terme où elles apparaissent, si encore elles le sont. L’instanciation des variables reste nécessaire. Comme même pour vérifier des termes constants, une résolution peut alors être nécessaire, la preuve de la satisfiabilité des règles, pour éviter les recherches de solution partant en récursion infinie parce que n’aboutissant jamais, reste nécessaire aussi.

Justement, à propos de la preuve de la satisfiabilité des règles, dans la proposition de la poser en général avec des hypothèses, comme fait en Novembre 2020, il y avait une faiblesse qui n’avait pas été abordée.

Un fragment de l’exemple était :


La conjonction « (poly P) & (digit D) » peut être démontrée satisfiable avec les hypothèses §h-poly-b et §h-digit, seulement parce qu’il n’y a pas de variable liant (poly P) et (digit D). Si les deux termes avaient une variable en commun, il ne suffirait pas d’apporter la preuve que chacun des deux termes est individuellement satisfiable, il faudrait apporter la preuve que la conjonction des deux est satisfiable. Excepté le faire avec un exemple de terme constant, je ne vois pas. Le faire avec un exemple de terme constant vérifiant la règle est suffisant pour la preuve qu’elle est satisfiable, mais se poserait un problème avec l’utilisation des hypothèses dont ce serait un cas, mais ce n’est pas le moment pour ça.

Bref retour sur la négation de la sérénité.

L’idée de la négation comme l’interprétation d’un jugement, peut faire penser qu’elle est un interprétation d’un jugement, comme n’importe quelle autre. On peut considérer que dans une conjonction, chaque terme est censée vérifier un jugement implicite, habituellement pas noté, parce que le plus fréquent. Ce jugement serait « vérifié ». La négation, « non‑vérifié », n’aurait rien de spécial en comparaison, juste que comme elle est moins courante, elle ne serait pas implicite et serait toujours écrite. Pour bien signifier qu’aucun des deux jugements n’a un status particulier par rapport à l’autre, excepté d’être plus fréquemment attendu, il serait possible de permettre d’écrire explicitement qu’un terme vérifie le jugement « vérifié ».

À moins qu’il ne fasse conserver le contexte courant inchangé, un terme peut produire un nouveau contexte, comme ça a été beaucoup souligné pour la négation et expliquer ce qu’elle ne peut pas signifier. Ce jugement qui ressemble à un opérateur unaire, pourrait s’écrire à droite du terme, c’est à dire à sa suite, ce qui évoque mieux l’idée d’un contexte produit par le terme pour ce jugement, au moins si on lit de gauche à droite (si on lit de droite à gauche, il devrait être placé à gauche) ; après le terme sans le sens de la lecture.

Justement, une notation y ressemblant avait été rencontrée, pour poser un jugement. Elle était de la forme « P true » pour dire que P est jugé true. De la même manière, au lieu de non P, il serait plus évocateur d’écrire P false, pour souligner que après ce terme et pour ce jugement, on a un contexte correspondant. C’est plus évocateur qu’une notation en préfixe, parce que le contexte qu’on a après le terme, dépend du jugement qu’on dit attendre, pas du terme seul. Si ce n’est pas convaincant, une autre raison est que écrire P true est assez proche de P is true, qui se lit bien. De même P is false se lit mieux que non P, juste que P is false est écrit P false.

Comme true et false peuvent être trompeurs, d’autres noms seraient choisis.

Cette idée de jugement habituellement implicite, explicitement représenté, sera introduite dans la nouvelle définition du langage de base, comme il est prévu de permettre de distinguer les cas où une vérification a une seule vérification des cas où elle en a plusieurs, autant que de permettre de confondre ces deux cas. Pour le moment, aucune idée de comment ils seront appelés.

Ici, le mot jugement est utilisé d’après ce que je crois en avoir compris. Les notions récemment introduites, s’apparentant à des appréciations ou à des qualifications, sont appelées ici, des jugements, en espérant que c’est un usage correcte du mot.

Je ne sais pas si le mot jugement convient parfaitement, parce que tel qu’il doit se comprendre ici, il a une particularité : il n’est pas toujours déterminé à priori.

Dans le cas de la vérification d’un terme constant, un jugement comme « vérification unique » ou « vérification multiple » ou « vérifié », ce dernier confondant les deux premiers, ces jugements là, serait déterministe. Mais en présence de variables libres ou ayant un certain degré de liberté au moins, le jugement ne serait pas déterministe. par exemple ayant A & B false, après B false, on serait bien dans un contexte vérifiant A & B false, sans aucune ambiguïté, mais si B contient des variables libre, c’est à dire que si B n’est pas entièrement déterminé, après A, il serait autant possible d’avoir B true que B false. B true signifierait une résolution produisant un contexte vérifiant B true, B false, une résolution produisant un contexte vérifiant B false, mais sans garanti que le contexte puisse être produit. L’échec de la production d’un tel contexte, serait un jugement lui‑même. À la suite de B true ou B false (hors échec), B pourrait être cette fois déterminé ou toujours pas.

Ce qu’il faut retenir, c’est que les jugements seraient prédéterminés ou non‑prédéterminés, selon le terme ou selon le jugement, dans le cas non‑prédéterminé, avant un terme, un jugement serait autant possible qu’un autre pour ce terme, le contexte correspondant étant produit ou ne pouvant pas l’être et s’il l’est, il l’est après le terme et le jugement. Certains jugement pourraient être une interprétation d’un jugement, comme « vérifié » pour aussi bien « vérif. unique » que « vérif. multiple ».

Pour plus de lisibilité, peut‑être faudrait‑il souligner la non‑prédétermination d’une manière ou d’une autre. Parce qu’il serait facile en lisant, en voyant un jugement, de lire en comprenant que c’était le seul possible, en comprenant qu’un autre était impossible.

Sur le paradox du menteur.

Il a été dit que dans le langage défini ici, une règle ne peut pas en empêcher une autre de vérifier ce qu’elle vérifiait déjà. Le cas où la seconde dépend de la première, ne le contredit pas non‑plus, comme la seconde n’est pas réalisable avant la première.

Il a été dit que quand on dit les faits, on ne ment pas. Une autre formulation pourrait être : le reniement d’un fait posé n’est pas un fait posé.

Dans le reniement d’un fait, on peut quand‑même voir un fait, celui du discours ou de ce qui est écrit. On peut aussi se dire que ce reniement est peut‑être légitime, si le fait posé n’est effectivement pas correcte d’une manière ou d’une autre. Mais même dans ce cas, ça reste un fait du discours, pas un fait posé ou plutôt un fait supposé.

Comme l’interprétation du reniement d’un fait dépend de la validité des faits, ça pose justement la question de leur validité, de ce qui est considéré comme un fait avéré. On peut dire que la validité des faits est une question autant importante que la possibilité ou non pour un langage, de renier un fait.

Ici, un fait, c’est un terme validé par les règles. La validité des faits dépend de l’interprétation de ces termes validés. Le langage ne s’en occupe pas, il ne le peut pas, il suppose que l’interprétation des faits est correcte et n’offre seulement pas de possibilité de les nier.

Introduction de l’idée de niveau de langage.

Précédemment, le mot courant en logique, « jugement », a été introduit, mais avec des doutes sur son bon usage, surtout dans les cas indéterminés pour cause de termes indéterminés. Un autre mot qui était plusieurs fois venu spontanément, « status », serait peut‑être plus facile à lire et à comprendre. Parler de constat pourrait convenir aussi, juste que ça se décentre du terme pour se centrer sur la justification. Peut‑être l’un ou l’autre selon le point de vue du moment.

Il a été dit que ces status sont des interprétations ou peuvent être interprétés comme d’autres status. Cette interprétation n’est pas la même que celle dont il avait été question jusqu’ici. C’est une interprétation de symboles (ou peut‑être parfois de termes, même si le cas ne s’est pas présenté), comme la précédente, mais une interprétation à priori interne, pas externe, une interprétation initialement définie pour le langage lui‑même.

Par exemple dans P true, la constante true, n’est pas destinée à apparaître dans un résultat renvoyé par une résolution ou pas destinée à apparaître dans un terme à vérifier. Ce serait une autre justification à dire que P true n’est pas un terme, que c’est P, qui l’est. Sans cette distinction, il pourrait y avoir un mélange entre l’interprétation interne au langage et l’interprétation externe.

Les status ou les jugements ou les constatations, selon lequel de ces mots convient le mieux, pourraient se comprendre comme des règles appliquées aux termes des conjonctions et des requêtes. Par exemple, P true pourrait se comprendre comme (true P), la règle correspondante et spécifique au langage, ayant été posée d’une manière ou d’une autre. On voit que ici, le terme habituellement externe, P, apparaît comme terme interne dans une tête de règle. On remarque aussi que true, qui est une constante spécifique à l’interprétation interne au langage, caractérise cette tête de règle.

Il y a deux domaines d’interprétation, même si ces deux interprétations ont des propriétés similaires. Pourtant, il pourrait être utile de faire une interprétation externe, de concepts internes au langage. Par exemple si un status est vérifié pour un terme, permettant de dire qu’il est déterminé, c’est à dire constant, ou indéterminé ou partiellement déterminé, ces faits pourrait être intéressants pour une interprétation à l’extérieur du langage, à condition de ne pas confondre les termes du domaine client du langage et les termes spécifiques au langage.

Un moyen agissant tout‑seul, de ne pas mélanger les interprétations, existe déjà : c’est la distinction entre termes internes et termes les plus externes, qui avait d’abord été remarqué avant de bien plus tard être remise en question. Ce qui a été remis en cause, était plutôt qu’un terme ne puisse apparaître que comme terme le plus externe ou que comme terme interne. L’exemple plus haut de (true P), montre que cette remise en question était utile. Mais justement, ce terme apporte la réponse à la question plus haut : P est un terme interne, (true P) est le terme externe, ils n’appartiennent pas au même domaine. Quand plus haut il a été dit que P true n’est pas un terme, disons que ce n’est pas un terme du domaine de l’interprétation des faits définis par les règles, plus précisément, des faits définis par les règles n’appartenant pas au langage lui‑même. « (true P) : … » serait une règle définie par le langage lui‑même, « (nat (s N)) : (nat N). » serait une règle définie par une l’interprétation externe, cliente du langage.

Le domaine définissant la règle « (nat N) : … », pourrait être appelé le domaine client ou le domaine usager ou le domaine d’application, du langage défini ici. Parler de langage objet pour le domaine usager, ne serait vraiment correcte que si on s’intéressait aux propriétés des règles qu’il défini, qu’on les étudiait. Ce n’est pas le cas ici ou pas pour le moment.

On a deux types de termes, ou même plus évocateur, deux niveaux de termes. Deux niveau, parce que l’un des types de terme peut apparaître comme terme interne de l’autre, mais pas la réciproque. On peut avoir (true (nat s N)), mais on ne peut pas avoir (peu-importe (true c)), en supposant que true n’a pas d’homonyme, qu’il ne désigne que celui introduit récemment. Si (peu-importe (true c)) apparaît quelque part, alors ce true, ne peut pas être celui du langage défini ici, ça ne peut être qu’un homonyme.

Si (true (nat s N)) peut être posé et a une interprétation interne au langage, apparemment rien n’interdit que (true (nat s N)) puisse aussi avoir une interprétation externe, cette éventuelle interprétation externe, quoi qu’elle soit, n’ayant aucune influence sur les interprétations internes du langage. On pourrait être tenté de dire qu’il ne faudrait juste pas mélanger les deux, ça se défend, mais ce risque ne fait pas une raison d’empêcher une interprétation externe des concepts du langage, parce que ce n’est qu’un risque éventuel.

On se permet donc d’exposer ou de rendre possible une écriture comme (true (nat N)), ce qui permet de définir la vérification de (nat s (N)), sans qu’obligatoirement un mélange à ne pas faire ne soit fait. En plus de permettre de poser ce qu’est la validation d’un certain type de terme, ça permet aussi de formuler leur propriété. Une colle se pose quand‑même : comment représenter la vérification de (true (nat N)) ? On partirait dans une régression infinie. Il existe peut‑être une solution, mais remise à plus tard, parce qu’elle nécessite d’introduire la notion de résolution, qui pour le moment, sera probablement exclue du nouveau langage de base.

Si on peut écrire (true (nat N)), comment empêcher d’écrire (nat (true N)), en supposant que true n’est pas un homonyme d’autre chose ? Si le point d’entrée dans le langage est toujours une règle définie par le langage et non‑pas une règle définie par le domaine client du langage, alors les termes interprétés par le domaine client, entrent toujours comme termes internes et n’en ressorte jamais, si les règles internes au langage ne produisent jamais ce cas. Plus encore, il serait de même pour les règles défini par le domaine client, elles seraient des termes internes, du point de vue du langage et non‑plus des termes externes, comme ils apparaissent quand on se place du point de vu du domaine client.

Une illustration du dernier point, pour qu’il soit plus compréhensible. On écrit toujours règles ainsi :

(nat (z)).

On les écrit ainsi, quand on est du point de vu du domaine client. Mais du point de vue du langage, cette règle apparaîtrait plutôt d’une manière plus ou moins similaire à ça :

(rule (nat (z)) ()).

Le terme vide dans cet exemple fictif, représente le corps vide de la règle. En pratique, on aurait plutôt un terme rules, et une liste de règles. L’exemple plus haut doit être compris comme ceci : les règles et les termes du domaine client, apparaissent comme des termes internes, dans le domaine d’interprétation du langage. C’est comparable à la validation d’un terme par le domaine client. Quand on veut savoir si (s (z)) est un nat, on incorpore le terme (s (z)) dans un terme (nat …), ayant alors (nat (s (z))), qui sera le terme de la requête « (nat (s (z))) ? ». Ce que le domaine client fait avec ses termes pour les vérifier avec ses règles, le domaine du langage le fait avec les règles du domaine client, pour en faire les sujets de vérification d’après ses propres règles. Ce qui est une règle pour le domaine client, est un terme pour le domaine du langage. À noter : le domaine du langage ne sait rien de ce que le domaine client considère comme des termes, dans le sens où il n’en fait aucune interprétation, ce ne sont de son point de vue, que des objets abstraits qu’il ne peut faire que transporter.

La possibilité pour le domaine client, d’interpréter les concepts spécifiques au langage, n’est pas seulement souhaitable, c’est une nécessité. Une nécessité pour interpréter le status d’une requête ou pour définir ses propres règles.

Il serait possible de dire qu’un domaine client, instancie le langage pour un ensemble de règles (ensemble de règles, qui est un terme, du point de vue du langage), de même que pendant la vérification d’un terme, une règle est instanciée pour ce terme. Pour cela, le domaine client doit pouvoir produire le terme correspondant à l’ensemble de règles, et donc connaitre ce concept propre au langage.

Ceci, toujours en supposant que le domaine client ne fait pas de confusion entre les termes du langage et les termes dont il veut connaitre le status d’après ses règles.

Pour des raisons pratiques, les règles seront toujours écrites comme elles l’ont toujours été, l’assemblage des règles sous forme d’un terme pour le langage, étant réalisé implicitement et automatiquement, par la mise en œuvre du langage, et dans le cas où on les règles sont écrites pour les expliquer, elles sont sous‑entendu par ailleurs mise sous forme d’un terme pour le langage. Cette mise sous forme d’un terme pour le langage, n’a pas d’intérêt quand on ne s’intéresse qu’aux règles qu’on écrit pour un domaine, ce qui justifie que ce soit implicite. Mais si on s’intéresse à la définition du langage lui‑même, ça doit être posé explicitement.

Les règles définie par le domaine client, posent des constats qu’il est attendu que des termes vérifient, ce qui pourrait poser un problème en cas d’erreur de la part du domaine client. Les règles définies par le domaine client, devraient poser des termes du domaine du langage, comme par exemple le (true P) abstrait et donné en exemple. Une erreur du domaine client, pourrait produire des inférences incorrectes ou des termes non‑interprétable par le langage. Pour cela, il est aussi nécessaire que les termes représentant les règles du domaine client, ne soit pas passé au langage directement sous forme de termes du domaine du langage, mais soit préalablement interprété par le domaine du langage en vu d’en faire des termes du domaine du language, ce qui permet une validation. Une autre manière de le dire : le terme représentant les règles du domaine client, avec lequel le domaine client instancie le langage, doivent être écrit dans une syntaxe que le langage va interpréter pour les traduire en ses propres termes, garantie valides. De cette manière, si par exemple le domaine client pose qu’il attend qu’un terme vérifie un jugement qui n’existe pas dans le langage, l’instanciation du langage échoue. L’exemple pris est celui de l’erreur de mentionner un jugement qui n’existe pas, mais ça pourrait être n’importe quelle autre erreur.

Ça fait une bonne raison d’écrire P true au lieu de (true P), ce qui rappel que le P true est une écriture qui sera vérifiée par le langage avant d’en faire un terme (true P).

Peut‑être une piste, pour la preuve de la satisfiabilité d’une conjonction de termes dépendants l’un de l’autre.

Si T1 et T2 n’ont pas de variable en commun, la satisfiabilité de T1 & T2, peut être faite en apportant une preuve de la satisfiabilité de chacun des deux termes, individuellement. Le problème se pose quand ils ont une variable en commun. Voyons le ainsi : on pose la conjonction T1 & T2, non‑par telle‑quelle, mais en les remplaçant par les corps des règles correspondantes (en simplifiant, en pratique, ce serait moins évident, mais c’est pour l’idée). On aura alors une conjonction comme par exemple T11 & T12 & T13 & T21 & T22. Dans cette nouvelle conjonction, la situation ne sera pas nécessairement la même, les éventuels termes n’ayant pas de variable en commun avec un autre terme, pourront avoir une preuve de satisfiabilité individuelle. On note ces preuves et on retire les termes ainsi traités. S’il ne reste plus rien, on a fini. Sinon, on reboucle de la même manière et ainsi de suite. C’est une idée, sans garantie qu’elle ne pose pas certains problèmes, elle n’a pas été approfondie.