Les logiques : notes en vrac

Il a été vu qu’avoir l’impossibilité d’une impossibilité, serait une contradiction de la notion même d’impossibilité. Il a été noté que l’impossibilité peut être vérifiée par le contexte seulement, qu’il n’est pas toujours possible de produire un contexte la vérifiant. Il a été proposé que la négation ne se lise alors que comme « n’est pas vérifié », qui pose moins de problèmes. Par là, une chose a été clarifiée, un problème a été résolu mais pas en lui donnant une solution, seulement en le mettant sous le tapis.

Le problème maintenant : le contexte peut justifier le constat qu’une chose est impossible, mais on a plus aucun moyen de le remonter comme un jugement, le seul jugement négatif pouvant être formulé maintenant, étant le « non‑vérifié ». Ça ne suffit pas, ça ne remplace pas le constat de l’impossibilité. Il y a apparemment plusieurs notions de négations ; l’une d’elle est l’impossibilité d’une chose. Il faut bien finalement permettre de la poser, mais en ne confondant plus l’attente de ce constat et la production d’un contexte le vérifiant. On a vu qu’on ne peut pas attendre l’impossibilité d’une impossibilité, à moins de l’anticiper, c’est à dire qu’on ne peut pas attendre l’impossibilité d’une impossibilité déjà constatée. Soit, mais ça n’empêche pas de formuler qu’on l’attend, ça ne sera juste jamais vérifié, et alors pas contradiction. Il y a eu trop d’affolement en décidant de ne pas permettre de la formuler pour empêcher de formuler son attente quand elle ne peut pas être satisfaite, empêchant de permettre de formuler son attente quand elle peut être satisfaite.

Plus que ça, ce n’est pas qu’une commodité le rendant visible, c’est une nécessité.

La syntaxe de l’attente d’un constat par le domaine client, ne doit pas avoir la même syntaxe qu’un terme, étant donné ce qu’il existe un jugement (c’est à dire constatation) implicite par défaut.

Étant donné le terme (true P), comme serait‑il possible de savoir s’il s’agit du true du domaine du langage ou d’un true défini par le domaine client ? ((true P) étant implicite avec P écrit tout‑seul). La notation P true empêche l’ambiguïté, la différence de syntaxe empêche l’ambiguïté. Sinon, pour que l’attente d’un jugement puisse utiliser la même syntaxe qu’un terme, il devrait toujours être explicite. Même en imaginant qu’il n’y ait pas de jugement implicite par défaut, avoir une syntaxe différentes est plus lisible, parce que ça distingue bien les deux domaines, le domaine client et le domaine du langage.

L’idée que les termes écrits par le domaine client ne soit pas directement interprété par le domaine du langage, n’est pas intéressante et même une complication sans avantage concret pour ce qui est de l’interprétation du status des termes d’après les règles.

Dans l’exemple d’une règle du domaine client, formulant l’attente d’un statut pour un terme, ce statut n’existant pas dans le domaine du langage, si la règle échoue, c’est une conclusion correcte. Il n’est pas utile de définir une pré‑interprétation des règles ou des termes dans les règles du langage.

Cette idée d’une pré‑interprétation, serait dans le même esprit que vouloir définir des règles d’écriture ou une autre pré‑interprétation, empêchant des choses comme « (eq A a) & (eq A b) », qui est toujours impossible. On peut se contenter du fait que la règle ne sera jamais vérifiée, sans avoir besoin de relever avant de tenter de vérifier la règle.

En parlant de syntaxe, la syntaxe des termes n’a pas besoin de faire partie des règles du langage, non‑plus. Elle serait définie, mais à côté. Par rapport au langage et au domaine client, la syntaxe des termes pourrait être tenue pour une évidence, un fait incontournable de leurs univers, de la même manière que dans le notre, la structure de la matière est un fait incontournable, on ne vérifie pas que de la matière est bien organisée comme elle doit l’être, quand on en utilise.

Définir une syntaxe, signifierait qu’on fait une distinction avec d’autres choses pouvant se produire, par exemple une distinction avec une série de symboles au hasard. Cette notion n’existant pas pour le langage, il n’y pas besoin de distinguer des symboles formant des termes, de symboles formant autre chose ou rien de défini.

Là aussi, si on y tient vraiment, on peut considérer que si tentait de vérifier une règle sur quelque chose ne respectant pas la syntaxe d’un terme, la règle ne sera jamais vérifiée, ce qui est une conclusion correcte.

Comme dit plus haut, il ne s’agit pas de dire que la syntaxe n’a pas besoin d’être définie, il est seulement dit qu’elle n’a pas besoin d’être défini dans un univers où il n’existe rien d’autre et où donc la distinction entre des termes bien formés et autre chose, n’existe pas. Par contre, dans notre univers à nous, cette différence existe et dans cette univers là, cette syntaxe doit être définie.

La notion de jugement implicite pour un terme, est aussi abandonnée, il est considéré qu’ils sont toujours explicites et que quand on ne les note pas, c’est un sucre syntaxique qui défini la correspondance. Ce qui est noté ici P true, sera finalement un sucre syntaxique, correspond au terme du langage (true P).

Ces choix sont pour se concentrer sur l’essentiel et faciliter la définition du langage lui‑même.

Un effet secondaire théorique intéressant, est que ça autorise plusieurs syntaxes possibles, ayant toutes une correspondance avec celle des termes du langage, avec une indépendance du langage par rapport à ces possibilités.

Justement, ce type de règle ne devrait pas être vérifiable, pour le nouveau langage de base, dont une caractéristique est reformulée. Au lieu d’être destiné à la vérification des termes constants, il est destiné à la vérification sans variables indéterminées, ce qui implique sans résolution et seulement sur des termes constants. L’idée initiale était de le destiner à la vérification sans résolution, ce qui a trop hâtivement été formulé comme destiné à la vérification de termes constants, une condition insuffisante, mais qui était aussi une caractéristique implicitement attendue. Il s’avère que le destiner à la vérification sans résolution, serait encore insuffisant, parce que ça n’empêcherait pas les termes non‑constants. Étant donné la règle « (r A). », la requête « (r A) ? » est vérifiable sans résolution, mais ne s’applique pas à un terme constant. La condition de vérification sans variables indéterminées, garanti les deux : pas de résolution et des requêtes seulement sur des termes constants.

Si une règle est par exemple de cette forme :

(r A) : (s A B) & (t B).

La variable B n’est pas déterminée par l’instanciation et nécessite une résolution. Ce cas est exclus et la règle ne serait pas vérifiée. Que pourrait signifier le terme (s A B) ? Probablement que B serait une chose dérivée de A, comme une propriété ou une valeur de A. Deux possibilités sont distinguées pour B : soit ses valeurs possibles sont en nombre infini, soit ses valeurs possibles sont en nombre fini. Si elles sont fini, disons que si par exemple ces valeurs peuvent être b1 et b2, alors la règle peut être reformulée ainsi :

(r A) : (s A b1) & (t b1).
(r A) : (s A b2) & (t b2).

Cette fois, les variables sont toutes déterminées à l’instanciation de la règle.

Le cas où B a une infinité de valeur possible ne peut pas être représenté de cette manière. Dans ce cas, A étant déterminé, le B de (s A B) serait plus probablement une valeur dérivée de A, plus qu’une propriété dérivée de A. Ce cas ne pouvant être reformulée, il ne sera pas possible ; une telle règle pourra être écrite, mais ne sera jamais vérifié.

En plus du cas d’un variable apparaissant dans le corps d’une règle mais pas dans la tête de la règle il y a le cas plus suspect d’une variable apparaissant dans la tête de la règle mais pas dans le corps de la règle.

Par exemple :

(r A B) : (s A) & (t A).

Dans ce cas, la variable B ne pourra pas être indéterminée, elle le sera nécessairement par l’unification. Ce cas est potentiellement douteux (à vérifier quand‑même, il existe peut‑être des exemples justifiés de tels cas), mais la variable B n’étant pas indéterminée, la règle pourrait être vérifiée.

L’idée de ne pas vérifier les règles contenant une variable indéterminée après instanciation de la règle, est pour ne vérifier que des règles vérifiables sans résolution. L’idée de ne vérifier que des règles vérifiables sans résolution, est pour avoir un langage de base le plus épuré possible et voir ce qu’il est quand‑même possible de formuler avec, entre autre, voir s’il pourra se définir lui‑même ou pas. Même s’il ne le peut pas, ce langage épurée permettra peut‑être de noter des notions qui n’avaient pas encore été remarquée. Des exemples ont été données, de notions manquées pour la raison de s’être précipité trop hâtivement dans l’idée d’un langage destiné à la résolution.

Il sera aussi tenté d’enrichir le langage autant possible, au delà du langage de base, sans introduire la résolution et la repousser autant que possible.

Le sens de l’exclusion d’une exclusion.

Dans une résolution de la négation par exclusion de possibilités pour une variable, si par exemple les constantes a, b et c sont exclues pour A, alors l’exclusion de cette exclusion, signifie qu’il est est exclus que a, b et c soient exclus de A, pas qu’on retire ces constantes d’une éventuelle exclusion déjà posée, sinon on a le paradoxe précédemment exposé. Disons qu’on appel cette exclusion, e. Si la variable A a initialement cette exclusion dans un contexte, l’exclusion de cette exclusion est incompatible avec le contexte, c’est à dire, impossible. Mais si A est initialement indéterminée ? Il faudrait pouvoir dire que A doit pouvoir inclure e. Alors en plus de la notion d’exclusion pour une variable, il faut aussi avoir une notion de non‑exclusion.

De cette manière, la conjonction d’une double négation et d’une simple négation se conclue de manière cohérente par un échec, quelque soit l’ordre des deux.

Si A est initialement indéterminée, qu’on exclus l’exclusion e, alors le contexte dit que A doit pouvoir inclure e. Si ensuite on pose que A doit exclure e, il y a incompatibilité et échec. Et ça marche dans l’autre ordre. Si avec A indéterminé, ont pose que A doit exclure e et que ensuite on exclus l’exclusion e, alors il y a incompatibilité et échec.

Pouvoir poser une exclusion pour A ne suffit pas pour interpréter la négation, il faut aussi une notion d’exclusion d’exclusion, ou dit d’une autre manière, pouvoir poser l’inclusion requise.

L’exclusion de l’exclusion de e pour A, n’est pas A, parce que poser que A doit pouvoir inclure e, n’est plus A entièrement indéterminée.

Donc on a bien non non P qui n’est pas équivalent à P.

Pourtant on a toujours une différence entre le cas où A est supposée initialement indéterminée et le cas où A est supposée pouvoir être n’importe quel terme pouvant être écrit, le fameux Any. Dans le cas où A est supposée indéterminée, poser que A doit pouvoir inclure e, détermine partiellement A. Dans le cas où A est supposée pouvoir être n’importe quel terme, poser que A doit pouvoir inclure e, ne change rien pour A.

Donc on a bien une interprétation différente de non non P, selon que être libre, pour une variable, signifie soit être indéterminée, soit pouvoir être n’importe quel terme pouvant être écrit.

Il n’y a apparemment plus de doute maintenant, que la question à résoudre est seulement celle du sens d’une variable libre. Une variable libre, doit‑elle être indéterminée ou être Any ?

La seule existence de cette question qui n’a pour l’instant pas de réponse, est une bonne raison d’avoir un langage de base ne vérifiant pas les règles se trouvant dans ce cas. Mais peut‑être la conclusion d’une telle vérification devrait‑elle être « indéterminé » plutôt que « échec » ou « non vérifié ». Ce serait même une nécessité, pour ne pas introduire d’incohérence avec la négation. Une autre option est de poser que ces règles ne sont pas valides, ne doivent pas être écrites. Si leur conclusion est indéterminée, alors c’est inconditionnellement et alors une règle se trouvant dans ce cas ne se distingue pas d’une autre règle se trouvant dans le même cas, c’est à dire, qu’elles ne se distinguent entre elles, en aucune manière. Inutile de les écrire. Pourtant, permettre de les écrire et les faire se conclure inconditionnellement par un statut « indéterminé », présente deux avantages : la définition du langage est plus simple et un concept potentiellement intéressant est introduit dans le langage.

En fait, ce n’est pas encore tout à fait clair, cette interprétation de l’exclusion de l’exclusion, pose peut‑être un nouveau problème, mais ce sera pour plus tard.

Quoiqu’il en soit, ce qui est impossible dans un contexte, doit être impossible dans un contexte dérivé (dit autrement pour s’amuser, l’impossibilité d’une impossibilité, est une impossibilité). Ce serait une manière formelle de dire qu’un contexte dérivé est identique ou plus restreint que le contexte dont il est dérivé. Une chose possible dans un contexte, peut cependant être impossible dans un contexte dérivé, mais ce n’est qu’une possibilité, pas une possibilité garantie, certaine chose possible ne pouvant que toujours être possible. Par exemple l’égalité d’une chose avec elle‑même, ne peut pas devenir impossible dans un contexte dérivé. Mais ces remarques sont peut‑être à réviser d’après le sens donné aux variables libres.

Cette interprétation, illustrée comme ça, est sensée, on ne peut pas la dire incorrecte dans ce contexte restreint, mais elle ne peut être que partiellement correcte. Au mieux, elle illustrerait une propriété que devrait vérifier la double négation, mais sans qu’on ne puisse en faire une définition.

Le problème est que cette interprétation de not‑not, fait de not‑not une chose en elle‑même, indépendamment de not tout‑court. Concrètement, not not P s’évalue sans évaluer not P. À la limite, pourquoi pas, mais ça ne tient plus quand la double‑négation est indirecte.

Ça avait déjà été suggéré, mais un terme employé plus tard disait le contraire : la négation n’est pas comme un opérateur prenant l’évaluation d’un terme en argument, la négation modifie plutôt la manière d’interpréter un terme, elle ne serait pas une chose réalisée après l’évaluation d’un terme. Dit intuitivement, la négation serait injectée dans le terme. De cette manière, le problème plus haut serait peut‑être résolu, la négation étant injectée dans l’évaluation du terme, la double‑négation apparaît directement comme telle dans l’évaluation du terme. Ce serait au moins compatible avec la remarque déjà faite, que la négation ne semble pas avoir de sens sans connaitre le sens du terme. Injecter la négation dans le terme, poserait bien qu’on ne dissocie pas la négation du sens du terme, que la négation n’a pas de sens concret en elle‑même.

Voir la négation comme une interprétation d’un terme, implique que l’écriture d’un terme, pose toujours deux significations : une signification positive et une signification négative, même en l’absence de toute négation. Non, trois : en plus des deux précédentes, il aurait une interprétation pour la double‑négation.

Il existe peut‑être une manière de voir cette triple interprétation, faisant plus sens. Un terme a une interprétation, « normale », et deux autres interprétations implicites, l’une étant les conditions de la garanti de sa vérification et l’autre étant les conditions de l’impossibilité de sa vérification. Mais est‑ce vraiment possible, vu que au moins (eq a a), ne peut jamais être non‑vérifié ? Ou alors, cette idée peut être révisée en considérant que ces conditions n’existent pas toujours, ce qui ne serait pas plus étrange qu’un terme auto‑contradictoire, ne pouvant jamais être vérifié.

Not‑not, ça rend knot‑knot …

Apparemment, pour une logique, le sens qu’elle donne à la double‑négation est plus déterminant que le sens qu’elle donne à la négation. Pourtant, difficile d’imaginer que le sens de la négation puisse se conclure du sens de la double‑négation, celle‑ci supposée posée. Pas plus facile de constater que le sens de la négation étant posé, le sens de la double‑négation ne se conclue pas facilement.

Il faut ancrer cette question dans la réalité ordinaire, pour que ça ne soit pas qu’un calcul sans signification. Ça a déjà était fait, et une conclusion (la seule pour le moment) a été qu’une impossibilité étant constatée, on ne peut pas rendre l’impossibilité à nouveau possible (ou alors ce n’était pas une vraie impossibilité), parce que ça contredirait la notion même d’impossibilité ; ou au moins, on ne peut pas le faire dans un contexte dérivé, et justement ici, on dérive un contexte d’un contexte précédent, on ne crée pas des contextes parallèles dissociés, et le contexte dérivé doit être compatible avec le contexte précédent, ne pas le contredire. En même temps, cette non‑contradiction n’avait été définie que pour une certaine résolution (remise en question pour le status de ses variables libres), sans négation. Cette non‑contradiction se résumait à ceci : la liaison d’un variable à un terme (à un terme, seulement, pas à son développement), n’est jamais changée dans un contexte dérivé. Peut‑être qu’avec la notion de négation, la notion de non‑contradiction du contexte précédent, doit être revue. Peut‑être que cette propriété de l’impossibilité en est une définition. Est‑elle suffisante ?

L’idée d’injection de la négation dans un terme, peut mieux se comprendre de cette autre manière équivalente : en présence d’une négation, le terme est évalué sous la négation, même si elle est indirecte. Ce ne serait pas plus étrange que d’évaluer un terme sous un contexte. Excepté que la négation ne ferait pas parti du contexte à proprement parler, ce serait une enveloppe n’existant que pour l’évaluation du terme.

Le négation serait bien comme un opérateur, mais comme rappelé, pas comme un opérateur prenant le résultat de l’évaluation d’un terme en argument, ce serait un opérateur agissant sur l’évaluation.

La négation à proprement parler, ne serait alors pas un jugement, même si elle se constaterait par un jugement (ce qui a déjà été suggéré à propos de l’impossibilité). C’est peut‑être cette double‑facette qui fait qu’on peut s’y perdre. Ce ne serait pas plus surprenant que le fait que la résolution vu jusque maintenant et le constat de son succès, sont deux choses différentes. Mais pourquoi ça ne perturbait pas autant ? Qu’est–ce qui fait que ça perturbe, seulement avec la négation ? Peut‑être est‑ce pour cette raison : avec une vérification déterministe de termes constants, la négation peut se résumer au constat (ou jugement, toujours pas de certitude sur l’usage du mot) de l’échec de la vérification, mais pas le négation avec une résolution. Aussi, en l’absence de négation, la résolution est plus proche de la vérification déterministe, que ne l’est la négation avec résolution, de la négation déterministe de termes constants.

Ça tourne souvent en rond, mais parfois ça progresse d’un petit pas.

Un petit progrès caché derrière une colle d’abord posée devant. Dans la triple interprétation d’un terme proposée précédemment, on pourrait voir une contradiction avec ce qui a été dit avant. Il a été dit qu’une chose impossible ne peut pas être rendue possible. Ors, une des trois interprétations d’un terme, serait les éventuelles solutions garantissant sa faisabilité, c’est à dire excluant sont impossibilité. N’est‑ce pas contradictoire ? Non, et la raison est : il n’est pas possible de rendre possible une chose qui a été constatée impossible. L’important est là : c’est si elle est déjà impossible, qu’elle ne peut pas être rendue possible. Reprenons longuement l’analogie de la porte, avant une conclusion plus loin, une porte que pour une raison inexpliquée, on veut rendre impossible à fermer. On cloue une planche devant le battant de la porte. On suppose pour l’image, qu’on a aucun moyen de retirer cette planche, qu’il est alors garanti que la porte ne sera jamais fermée. Il a été dit que dans ces conditions, si quelqu’un arrive à faire en sorte de fermer la porte, alors elle n’était finalement pas impossible à fermer. Par là, on illustrait que si une chose supposée impossible est rendue possible, alors ce n’était pas une impossibilité, dit autrement, rendre possible ce qui est impossible, est auto‑contradictoire, dans le sens où cela nie le sens de l’impossibilité. Il avait été fait remarquer que si on voulait empêcher de fermer cette porte vraiment impossible à fermer, alors ça ne serait possible qu’en agissant en amont (autrement dit, un voyage dans le temps), c’est à dire que le second vœux d’impossibilité, devrait avoir lieu avant le premier, mais que alors le premier se trouvant en second, pour avoir du sens, devrait faire de même et se placer en premier, et l’autre ferait de même et comme ça sans jamais aboutir à rien. Mais ceci ne vaut que parce qu’on est dans un contexte où on voudrait rendre impossible, une impossibilité déjà existante.

Un détail important a été manqué : si on a un terme T qu’on vérifie par une règle R, dans la vérification de R, le terme T n’est pas encore vérifié (*). Si le terme T est en négation et que R vérifie un autre terme en négation, la négation de ce terme dans R, ne fait pas partie du contexte de T, puisque T n’est pas encore vérifié. On est dans le cas où on anticipe une impossibilité et qu’on souhaiterait poser les conditions de son impossibilité. C’est à dire que non non P n’est pas la même chose que P = non Q, en vérifiant non Q, suivit de non P, qui ne pourrait pas être vérifié. Mais lieu de ça, on pourrait vérifier non non Q (sous réserve de solution, mais disons que ça ne serait pas un échec assuré).


(*) T n’est pas une une hypothèse, parce qu’une hypothèse n’est pas vérifiée, elle est tenue pour vérifiée.