Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 15 Mar 2022 03:32
Message Re: Les logiques : notes en vrac
Penser à revenir sur le problème rencontré avec une démonstration à propos de neq.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 15 Mar 2022 11:58
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Avec un doute que c’est peut‑être en partie une répétition, autant que c’est peut‑être une idée pas encore écrite.

Il pourrait être intéressant d’envisager de remplacer l’indétermination d’une variable, par une hypothèse, en notant qu’un terme partiellement déterminé, contient toujours au moins une variable entièrement indéterminée (c’est le cas de base).

[…]

— Édit : cette idée conviendrait peut‑être mieux pour la double et la simple négation, ou alors si on considère que les solutions sont toujours présentées ainsi, alors il n’y a plus de différence entre la double négation et l’absence de négation. Mais là encore, ce n’est qu’une vague idée. —

Il avait été noté que les triples négations se simplifient en simple négation, jusqu’à ce qu’il ne reste plus qu’une double ou simple négation, ou encore, que les double négations s’annulent excepté la dernière. Ce qui était dit dans le message cité, suggère une troisième formulation, proche de la seconde plus haut : sous une double négation, les double‑négations s’annulent.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 15 Mar 2022 14:30
Message Re: Les logiques : notes en vrac
Penser à ne pas oublier de revenir sur la question de la définition et de l’usage des équivalences.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 15 Mar 2022 15:42
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Idée de formulation : une hypothèse peut prendre la place d’un terme mais ne peut pas rester à la place d’un terme ; un terme peut prendre la place d’une hypothèse ou d’un autre terme et y rester ; quand une hypothèse prend la place d’une hypothèse, c’est en prenant la place d’un terme.

Aussi, un terme peut se substituer à une conjonction (écriture des règles et sens des termes) autant que la réciproque (résolution).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 15 Mar 2022 22:34
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Ce n’est qu’une idée vague sur un problème malheureusement compliqué. S’il n’a pas de solution, l’idée des constats supplémentaires en plus des true et false implicites, sera abandonnée. Après avoir repris à la suite du paragraphe précédent, il faudra se poser la question des constats sur des relations entre deux termes, comme T1 plus spécifique que T2.

Le paragraphe en question, était sur l’approche qu’est de donner à la paire de constats const/var, le même comportement que la paire de constats false/true. Là où ça en était : comme false, const reste dans les contextes dérivés, comme true peut devenir false dans un contexte dérivé, var peut devenir const.

Il avait été dit que const est la forme négative de var, par analogie avec false qui est le négatif de true. Mais le mot n’est pas parlant. Parler de forme persistante serait préférable. False et const sont deux constats persistants qui une fois fait, ne peuvent plus changer, true et var sont deux constats qui ne persistent pas nécessairement.

L’avantage qu’il y a à le noter, est que dès que T const a été constaté, il n’est plus nécessaire de le tester à nouveau dans les contextes dérivés. Mais T var, nécessite d’être tester chaque fois que le contexte change. Pourquoi cela, alors qu’on a rien de tel avec true ? Ben si, on a quelque chose de tel, true est vérifié à chaque changement de contexte, et cette vérification fait même partie du processus de dérivation d’un nouveau contexte. La différence est ailleurs, true est un constat implicite (*), quand une unification est un succès, true est implicitement constaté, et false dans le cas contraire. Mais il y a plus. Imaginons qu’on décore tous les termes d’un true explicite, comme par exemple A true & B true & C true. Si au lieu de true, le constat était var, chaque fois que le contexte change, il faudrait re‑tester le constat sur chaque terme pour lequel il est attendu. C’est différent pour true. Si une résolution porte sur C, la résolution est de telle sorte qu’elle ne peut pas contredire le constat true de A et B et alors il n’y a besoin pour tester true, de re‑tester true sur les trois termes chaque fois que le contexte change, comme par exemple après la résolution de C. C’est différent avec le constat var, qui n’est pas lié à la résolution, il est plus difficile de savoir, en résolvant par exemple C, de savoir si sa résolution est en train de remettre en cause un éventuel constat var qui aurait été fait sur A ou B.

(*) Il est possible de le voir autrement, de considérer que que les constats implicites sont succès et échec, qui sont exposés comme true et false et qu’il existe un autre constat, qui est celui pour une solution d’être retenue ou pas, mais c’est aller trop vite, ce que ça signifie sera expliqué plus loin.

Même si l’évolution de var et const à travers les contextes, a comme modèle, l’évolution de true et false, le test de var ne peut pas se faire de la même manière qu’avec true. Il serait possible d’imaginer qu’une certaine mise en œuvre fait usage de diverses astuces pour, en même temps qu’elle résous un terme, savoir si cette résolution remet en question un constat var fait sur un autre terme. Ce serait peut‑être possible (sans nécessairement en valoir la peine), mais ça n’aurait pas de place dans une description de la sémantique, comme ce n’est pas obligatoire, ni pour une mise en œuvre, ni pour la sémantique et que comme avec tous les détails internes, la solution est potentiellement largement variable. Il y a une autre raison : ça ne pourrait pas être une approche générale, à cause de deux autres constats intéressants à faire, la relation de spécificité ou l’absence de relation de spécificité.

Var et const évolue de manière monotone, l’évolution ne se fait que dans un sens, de var vers const et ne change plus après const. Peut‑on imaginer une situation si peu commode que dans un contexte, un constat est vérifié, dans le suivant il ne l’est plus, dans le suivant, il ne l’est toujours pas, mais dans le suivant, il l’est à nouveau ? Oui, et c’est un exemple de ce qu’il peut se produire avec la relation de spécificité. Elle implique deux termes et selon l’ordre dans lequel la résolution est faite plus ou moins partiellement sur ces deux termes, le constat pourrait évoluer en alternances irrégulières, comme imagé plus haut. Imaginons que qu’on attende le constat que T1 est plus spécifique que T2 (aucune notation n’est encore prévue pour un constat portant sur deux termes). Imaginons que le constat soit vérifié en toute fin de résolution, c’est à dire à la conclusion d’une requête. Le constant dépend de la résolution finale de T1 et de la résolution finale de T2. Mais imaginons maintenant plusieurs cas possibles pendant la résolution. T1 est résolue pas à pas, jusqu’à sa solution définitive, puis T2 de même, ou l’inverse, ou T1 est résolu partiellement en deux étapes, puis T2 en trois étapes, etc. À chaque fois, il serait même inutile de tester le constat attendu, le constant sur les étapes intermédiaires de la résolution, n’augurant rien du constat final. Pour cette raison, même si l’approche proposée pour les constats var et const était assez plaisante, elle n’est pas assez générale pour couvrir le constat maintenant discuté. Il n’y aurait aucun intérêt à faire une différence entre ces constats, comme de toutes manières, ils peuvent tous être réduits au constat final, même si certains peuvent être connus plus tôt.

Donc la sémantique des constats sera ainsi : ils sont testés en toute fin de la résolution réussie d’une solution candidate, si un seul constat n’est pas celui attendu, la solution n’est pas retenue. Le test est effectué sur le terme sur lequel il a été posé, et le test est effectué dans le contexte qui est la solution candidate (sous entendue, terminée avec succès). La note qui suit ne fait pas partie de cette description. On a vu que pour couper un certain type de récursion infinie, on retient les termes en cours de résolution, que l’on tient comme signifiant leur solution définitive, même si cette solution n’est pas encore connu ; il en est de même ici. Les termes sur lesquels les constats sont posés, sont retenus tels‑quels, et le test est effectué sur le terme tel‑quel dans le contexte qu’est la solution candidate.

Ce sujet n’est encore pas résolu, loin de là. Il reste encore à aborder :

  • L’intégration des constats dans les négations, qu’elles soient simples ou doubles.
  • Les constats dans les démonstrations.
  • Les constats et les hypothèses.
  • Le constat de l’unicité ou de la multiplicité d’une solution.
  • Le constat d’une conclusion indéterminée à une vérification (ce que ça signifie sera rappelé au moment d’y revenir).
  • Le point précédent rappel que les constats n’aboutissent pas tous à la sélection ou pas d’une solution, ils peuvent être un attribut d’une solution.
  • La réinterprétation de constats, c’est à dire des constats à partir de constats.
  • La question des notations, comme par exemple pour les constats portant sur deux termes, mais c’est une question d’une autre nature, elle n’est pas préoccupante.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 17 Mar 2022 14:43
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
  • L’intégration des constats dans les négations, qu’elles soient simples ou doubles.
  • […]


Dans ce qui suit, la formule « not A const » est tenue pour signifier « not (A const) » ; la raison de ne pas la tenir pour « (not A) const » sera expliqué juste après la conclusion de ce message.

Ce qui suit est un petit peu long, mais la conclusion est très brève. Un point est sujet à possible remise en question.

Disons qu’on a A const, qu’on veuille en poser la négation. Comment cette négation peut‑elle être vérifiée ? Peut‑être que spontanément, on croirait voir deux solutions : la négation de A et la non‑vérification du constat const ; chacun de ces deux cas garantissant que A const n’est pas vérifiée, ça pourrait avoir l’air cohérent. Mais ces deux alternatives posent chacune un problème. Dans la première, on assure la négation de A, alors le constat const, n’a à la fois, pas de pertinence et pas de sens. Pas de pertinence, parce que si A n’est pas vérifié, le constat n’a pas à l’être ; c’est une conséquence de la sémantique du constat, que cette approche ne respecte donc pas. Pas de sens, parce que un constat porte sur un terme résolu et ici, A n’est pas résolu. Dans la seconde alternative, le problème est que A pourrait être arbitrairement n’importe quel terme ne vérifiant pas le constat, alors que la négation signifie que A ne peut pas exister, ce qui serait contraire à la sémantique de la négation. Cette approche ne respecte donc, ni la sémantique du constat, ni la sémantique de la négation.

Le problème dans cette approche, est qu’elle interprète à tord, A const comme une conjonction. On a bien une conjonction d’un point de vue abstrait, à la fois la vérification du terme et à la fois la vérification du constat sur ce terme, mais voilà justement les deux ne sont pas dans la même situation : on vérifie le constat sur le terme et l’applicabilité du constat est conditionnée à cette vérification.

Il existe pourtant bien une interprétation respectant les deux sémantiques et elle est indiquée à la fois par le sens du constat et par le sens de la négation. Le sens du constat est d’être vérifié sur un terme résolu, tandis que le sens de la négation, est que le terme en question ne peut pas exister. Comme le constat est sensé s’appliquer sur un terme résolu et ne pas être testé dans le cas contraire, l’absence de terme résolu implique que le constat est sans objet, c’est à dire n’a pas à être testé.

Une reformulation du paragraphe précédent, avec une reformulation de la négation, différente sur un point de ce qu’il en a déjà été dit, mais conforme avec. La négation not A, signifie la garantie que A n’est pas possible, la double négation not not A signifie que A est garanti possible, sans dire ce qu’il est. Autant la simple que la double négation peuvent échouer. Si elle peuvent échouer, c’est parce qu’il y a résolution. Il y a résolution, mais pas sur un terme, au lieu de ça, sur un contexte seulement. Dans not A, le contexte est résolu de manière à ce que le terme ne puisse pas exister, il n’y a pas de résolution du terme, donc pas de terme A défini, donc un constat est sans objet. Presque de même avec la double négation à la seule différence qu’elle garantie que A est réalisable, elle aussi, ne résous pas A et ne résous que le contexte et alors là aussi, tout constat est sans objet.

En allant un peu vite, on pourrait croire que le constat const et le constat true par exemple, ne sont pas traités de la même manière, parce qu’il n’a jamais été question d’abandonner le constat true nul‑part jusque maintenant. Pourtant si, mais c’était implicite. Quand on écrit not (A true), le constat true est abandonné aussi, c’est même le but de la résolution de la négation, que de ne pas avoir de terme sur lequel pouvoir le vérifier. Il en est de même avec une vague interprétation de not (A false), false pourrait être intuitivement le but de la résolution et pourrait être vu comme omissible car redondant, et cette fois, la présence du constat false ne rend pas automatiquement la formule non‑satisfiable (*). Ceci dit, il ne faut pas oublier qu’ils sont aussi abandonnés parce qu’ils sont non‑applicables car sans objet, eux aussi, les constat true et false n’ont de particulier ici, que d’avoir une explication intuitive supplémentaire à leur abandon sous une négation.

(*) not A & A false n’est malgré tout par vérifiable, comme A ne peut pas exister sans contredire not A et qu’il ne peut donc pas exister de terme sur lequel vérifier le constat false, même si intuitivement, on pourrait comprendre la formule comme une tautologie. Ou alors, il faudrait donner à ce constat, un status particulier, mais mieux vaut éviter, pour ne pas compliquer les choses et risquer ainsi d’introduire des difficultés dans la définition pour un bénéfice presque nul, à moins que ça ne se montre nécessaire plus tard.

La réponse à cette question est donc : sous une négation, qu’elle soit simple ou double ou plus, les constats disparaissent parce qu’ils ne sont pas applicables, ni vérifiables, ni non‑vérifiables.

En marge, d’après les explications plus haut, il est possible de comprendre que « not A const » devrait plutôt se lire comme « not (A const) », plutôt que comme « (not A) const ». Dans le premier cas, on écrit d’abord A const, qui est pertinent, puis on ajoute not (A const), qui est pertinent mais fait abandonner le constat, ce qui équivaut finalement à not A. Dans le second cas, on écrit d’abord not A, qui est pertinent, puis ont ajoute (not A) const, qui est immédiatement non‑pertinent et est abandonné aussitôt écrit, ce qui équivaut finalement à not A, aussi. Autant not (A const) que (not A) const sont équivalents à not A, mais la première écriture a une fois et demi la pertinence de la seconde. Pour cette raison, il est décidé que les constats ont la priorité sur le mode de résolution, que not A const se lit not (A const).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 17 Mar 2022 15:32
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Une reformulation du paragraphe précédent, avec une reformulation de la négation, […]. Dans not A, le contexte est résolu de manière à ce que le terme ne puisse pas exister, […]

Quand il est question de résolution, il faudrait formellement comprendre, la résolution d’un contexte plutôt que la résolution d’un terme, la résolution du contexte ayant jusqu’ici trois buts possibles : donner une solution à un terme, garantir qu’un terme n’a pas de solution, garantir qu’un terme a au moins une solution. Alors parler de la résolution d’un terme est un abus de langage. Mais les termes, sont ce qui est écrit, contrairement au contexte, qui n’apparaît pas dans l’écriture, justement parce qu’il est ce qui doit être résolu et ne peut pas être posé d’avance. Pourtant, parler de résolution d’un terme ne pose pas de problème temps que c’est en voulant dire implicitement qu’on dérive pour cela un nouveau contexte.

Cet abus de langage acceptable est à ne pourtant pas oublier en cas de difficulté à comprendre certains choses, des choses pour lesquels se rappeler qu’on résous un contexte, aide à y voir plus clair, ce qui est justement le cas avec la négation.

C’est ce qui avait été manqué en abordant la question de la négation, qui se comprend mieux si on note que la résolution, est la résolution d’un contexte. Sans ça, la résolution de not A peut être difficile à comprendre, à moins qu’on ne fasse la correction spontanément sans y penser. Si voyant not A, on pense que la résolution de not A porte sur A, le sens même de la négation risque d’être mal compris : A n’est pas résolu, ce qui est résolu, c’est le contexte, résolu de manière à ce que A ne puisse pas y être vérifié. Le terme A est un bien impliqué dans cette résolution, mais ce n’est pas A qui est résolu.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 17 Mar 2022 15:47
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Ce qui suit est un petit peu long, mais la conclusion est très brève. Un point est sujet à possible remise en question.

[…]

(*) not A & A false n’est malgré tout par vérifiable, comme A ne peut pas exister sans contredire not A et qu’il ne peut donc pas exister de terme sur lequel vérifier le constat false, même si intuitivement, on pourrait comprendre la formule comme une tautologie. Ou alors, il faudrait donner à ce constat, un status particulier, mais mieux vaut éviter, pour ne pas compliquer les choses et risquer ainsi d’introduire des difficultés dans la définition pour un bénéfice presque nul, à moins que ça ne se montre nécessaire plus tard.

[…]

Le point du message, mentionné comme possiblement sujet à remise en question, était justement celui‑ci. Un constat se fait sur un terme, A false ne peut donc jamais être constaté, puisque il devrait être sur un terme, mais sans terme, pas de constat.

Il est préférable de ne pas remettre ce point en question, mais ça suggère qu’une chose manque : la possibilité de dire qu’un certain objet n’existe pas. Ce ne serait alors pas un constat sur un terme, mais un constat sur un contexte.

Il faudra donc probablement aussi penser à se pencher sur cette question : les constats sur un contexte, ce contexte pouvant éventuellement être le contexte vide.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 17 Mar 2022 16:02
Message Re: Les logiques : notes en vrac
Les constats tels que définis jusqu’ici, porte sur des termes, mais les exemples de terme, ont toujours été des interprétations. Si on peut écrire (r A) const, on ne peut cependant par dire qu’on attend que A seule soit testée const. Se pose un problème avec (r A) var par exemple, qui ne pourrait jamais être constaté.

C’est une question de syntaxe. Un constat doit avoir un nom, mais permettre d’écrire un constat dans un terme pour qu’il s’applique à un élément de ce terme, poserait un problème de confusion, soit avec les noms de variable, soit avec les noms de constante ; à moins de trouver une convention distinguant bien les noms de constats.

D’après le message précédent, il faudrait encore en plus, distinguer les constats portant sur des termes, des constats portant sur des contextes.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 17 Mar 2022 17:05
Message Re: Les logiques : notes en vrac
Il y a finalement, constats sur des termes et constats sur des contextes.

Hibou a écrit : 
[…] Un constat se fait sur un terme, A false ne peut donc jamais être constaté, puisque il devrait être sur un terme, mais sans terme, pas de constat.

Il est préférable de ne pas remettre ce point en question, mais ça suggère qu’une chose manque : la possibilité de dire qu’un certain objet n’existe pas. Ce ne serait alors pas un constat sur un terme, mais un constat sur un contexte.

Il faudra donc probablement aussi penser à se pencher sur cette question : les constats sur un contexte, ce contexte pouvant éventuellement être le contexte vide.


Comme constat sur un terme, false ne peut jamais être vérifié. Intuitivement, on peut pourtant y trouver un sens, même s’il est contredit par la définition donnée jusque maintenant. Les constats sont introduits pour exposer des notions sémantiques inaccessibles autrement, car ne pouvant pas être constaté par les règles, en particulier.

Le cas de false mis face à la raison de l’introduction des constats, fait dire que si, il préférable de remettre en question ce qui été défini, parce que c’est le seul moyen de remédier à la lacune relevée.

Correction avant plus de détails plus loin : il y a deux types de constats, les uns sur les termes, les autres sur les contextes ; false ne peut que être un constat sur un contexte.

Comment désigner un contexte ? Implicitement, par un terme vérifié, qui défini implicitement un contexte, celui le vérifiant. Mais si le contexte ne vérifie pas ce terme ? Eh bien un terme peut aussi être considéré comme désignant une catégorie de contexte ne le vérifiant pas, ce qui ne pose pas de problème, comme les constats sont sans résolution, qu’ils sont testés après la toute fin de la résolution d’une solution candidate.

Il faut ajouter à la liste d’interprétation des termes : un terme désignant un contexte. Plus exactement, un tel terme ne peut que être une interprétation, parce que le terme A dans (r A), ne désigne pas un contexte, c’est (r A) qui désigne un contexte, car c’est l’interprétation qui désigne la règle à vérifier et donc la résolution a effectué.

Les interprétations s’appliquant à un contexte, porterait sur un ou plusieurs termes qui sont des interprétations. Les interprétations portant sur un terme, s’appliquent à des termes internes autant qu’à des termes externes, même si la syntaxe permettant de les appliquer à des termes internes, n’a pas encore été décidée.

La sémantique des constats portant sur des termes, est comme définie jusqu’ici, elle ne change pas, y compris pour ces constats sous une négation. Justement, les constats, jusqu’à avant ce message, n’avait été envisagés que comme portant sur des termes.

Le constat false porte sur un contexte, mais aussi finalement le constat true. En effet, true vu comme un constat sur un terme résolu, ne dit rien sur ce terme, est une tautologie. Par contre, il dit quelque chose de pertinent sur un contexte. De plus, le constat true, vu comme un constat sur un terme, s’il est sur un terme interne, implique qu’il est vérifié sur le terme externe tout entier, l’interprétation, ce qui confirme d’une autre manière que true est un constat sur un contexte.

Un constat sur un contexte, est vérifié en toute fin de résolution sur le terme tel‑quel, dans le contexte qui est la solution candidate, comme pour les constats portant sur des termes. La raison est que sinon on a une dépendance à l’ordre des termes. En effet, si A false, cette fois vu comme un constat sur un contexte, dit qu’on attend que A ne soit pas possible dans le contexte, alors selon que ce fragment de formule apparaîtrait avant ou après un certain not A, la conclusion ne serait pas la même. Pour les conditions du test, les constats portant sur un contexte sont comme les constats portant sur un terme.

— Édit: ce paragraphe est en partie trompeur, pour la raison donnée dans un message suivant — Pour la négation, comme elle est une résolution d’un contexte, elle ne peut pas ignorer un constat portant sur un contexte. Si le terme A se comprend comme A true, si not A résous le contexte tel que A n’y soit pas vérifiable, alors not (A true) résous aussi le contexte tel que A true n’y soit pas vérifiable. Le plus sûr car faisant le moins de supposition, est de considérer que dans ce cas, A true ne doit pas être vérifié, plutôt que de considérer que A true est remplacé par A false, ceci, afin de couvrir le cas d’éventuels futurs autre constats sur un contexte. Ça signifie aussi qu’un mode de résolution d’un contexte, nécessite que lui soit associé un mode de vérification des constats portant sur un contexte. Là aussi, le cas le plus général est considéré, pour permettre d’éventuels futurs mode de résolution ultérieurs.

A false & not A serait vérifié, de même que not A & A false, du moins dans un contexte final vérifiant not A. Au contraire, A & A false ne serait pas plus vérifiable que A & not A, mais les deux ne seraient pas synonymes pour autant, même si l’équivalence devrait être démontrable. Bien que équivalents sous réserve de le démontrer, les deux ne serait pas synonymes, parce que dire qu’on ne vérifie pas A true, n’est pas littéralement la même chose que dire qu’on vérifie A false. En général, not A et A false ne sont pas synonyme non‑plus et il ne devrait cette fois pas être possible de démontrer une quelconque équivalence, A false étant sans résolution, tandis que not A implique une résolution. En particulier, en l’absence de toute résolution, comme par exemple dans une vérification sur des termes constants seulement, A false et not A doivent‑ils être considérés comme synonymes ? Intuitivement, il semble que oui, sauf à trouver un cas montrant le contraire.

Même remarque avec la négation, not (A false) résoudrait le contexte de manière à ce que A false n’y soit pas vérifiable, not not (A true) résous le contexte de manière à garantir que A true y est vérifiable, not not (A false) résous le contexte de manière à garantir que A false y soit vérifiable. Pourtant, not (A false) ne serait pas synonyme de not not (A true), mais il devrait être possible de démontrer que les deux sont finalement équivalents.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet