Les logiques : notes en vrac

L’équivalence logique n’est pas l’équivalence sémantique.

p ⇔ q signifie seulement une corrélation, c’est à dire que p et q sont simultanément, soit vrais, soit faux, pas que p et q sont la même chose (ou pas nécessairement).

Dans les théories des types dépendants, l’égalité et l’équivalence, ne sont toujours pas unanimement définis, même après quarante années de recherche.

Une définition n’est pas un axiome, une définition n’affirme pas l’égalité entre deux choses préexistantes, elle affirme l’égalité entre un mot nouvellement créé et une chose préexistante ou écrite en termes de choses préexistantes.

En supposant que A et B existent, affirmer A = B, c’est poser un axiome, mais écrire N = A, où N est nouvellement créé, ce n’est pas un axiome, c’est seulement désigner A par N.

HOL4 peut être sujet à l’inconsistance de Pollack. C’est le cas au moins avec une librairie pour définir des structures de données co‑récursives. Ce n’est pas un problème d’incohérence du noyau d’HOL4, c’est ce qui est défini par l’utilisateur, qui peut exceptionnellement ne pas être bien pris en charge par les fonctions de définitions des structures de données. Pour s’assurer de ne pas être dans ce cas, il faut définir et démontrer quelques propriétés que devrait avoir la structure de données définie. Mais si la démonstration échoue, on ne peut pas savoir si c’est parce qu’on comprend soi‑même mal la structure de données qu’on défini ou si c’est la librairie qui l’a mal interprété. Si ce problème existe, c’est parce que cette librairie est complexe.

L’implication causale, l’implication en logique linéaire, se note ⊸ , c’est le caractère Unicode U+22B8, nommé Multimap. Son nom suggère qu’il a d’autres usages aussi, il ne faut pas systématiquement l’interpréter comme l’implication linéaire sans s’assurer d’être dans ce contexte.

En plus du quantificateur universel, ∀x.P, du quantificateur existentiel, ∃x.P, il y a la quantificateur individuel, ιx.P, qui se lit « Le x tel que P ». La sorte de i dans la notation, c’est la lettre iota minuscule, le caractère Unicode U+03B9.

J’avais déjà vu cette lettre utilisée en logique, pour désigner « l’ensemble des individuels », mais je ne sais pas quelle est la définition de cet ensemble. Il y a sûrement un rapport entre les deux.

La différence ensembliste est parfois notée avec une barre oblique, mais pas celle de la division, l’autre : S\{e} pour dire S - {e}. Je préfère la seconde notation.

Un certain Gérard Berry pendant une conférence a dit en gros « avec l’algorithmique, c’est très facile de faire n’importe quoi, c’est très difficile de faire les choses correctement ».

Je ne l’ai pas attendu pour le savoir, mais ça fait un bol d’air que quelqu’un le dise explicitement.

Sans rapport avec l’application des logiques à l’informatique, je mentionne un livre répertoriant des preuves sans mots, en image : “ Proofs without words ”, de Roger B. Nelsen, édité par The Mathematical Association of America. Un premier tome a été publié en 1997, deux autres ont suivi plus tard.

Je ne trouve pas de page de vente du livre chez l’éditeur, je ne trouve que des liens Amazon, alors je n’indique pas de lien.

Les solveurs SAT et SMT, par des examples : SAT/SMT by Example (yurichev.com) [PDF], Dennis Yurichev, 2019; mis à jours quand il le peut.