Blog personnel d'Arthur Milchior

J'ai uniquement des résultats en rapport avec la logique sur des nombres. Sauf qu'une logique ça a plein de paramètres:

• Parfois c'est de la logique d'ordre 1, monadique existentielle, parfois de la logique d'ordre supérieur, voire de la logique d'ordre variable ! Et puis parfois je rajoute mêmes des opérateurs. de point fixe, de clôture transitive, déterministe ou non, et même alternant.
• En plus, mes modèles sont soit finis, en particulier sur les mots, soit sur les entiers, donc infinis, soit carrément sur les réels.
• Quant aux prédicats que je m'autorise, c'est simple, je ne prend jamais quelque chose de plus compliqué que l'addition. Je peux prendre les modulos, la relation d'ordre, le successeur d'un nombre... Enfin, quand je dis jamais, j'ai un résultat où j'ai aussi la multiplication, mais c'est une exception. Et puis la fonction «Partie entière» mais c'est pratiquement la même chose que l'ordre. Et puis les flèches de Knuth, mais ça c'est un accident, j'ai démontré qu'on pouvait l'avoir à partir de +1 et d'une fonction non interprétée.
• Oui, parce que j'ai certes des prédicats connus. Mais j'ai aussi des prédicats dont l'interprétation n'est pas fixée. Et puis aussi des prédicats non interprétés. J'y reviendrai plus tard.

Et puis j'ai plusieurs types de résultats:

• De la complexité descriptive, c'est à dire que je relie une logique et une difficulté de calcul. Dans mon cas les calcul qu'on peut faire avec un temps limité par une tour d'exponentielle.
• Des maths presque pures, c'est à dire que je décris de manière exhaustive certains types d'objets, des relations sur les entiers où les réels. Ou alors quand je ne peux pas les décrire, au moins je dis «Regardez, à partir de ça, qui est tout simple, je peux créer des trucs très complexes. Alors peut-être que ce premier objet n'était pas si simple qu'il en a l'air.
• Certains sont de la logique qui parle de la logique, ce qu'on appelle la «Définissabilité de la définissabilité», c'est à dire qu'on crée une formule dans une logique L qui dit «tel objet est définissable dans une logique L'». Même qu'en général, L est égal à L'.
• Enfin j'ai des résultats informatiques, quand même ! En particulier, quelques résultats d'indécidabilité - cas où j'ai prouvé qu'un ordinateur ne peut pas répondre à une question. En général, je dis «on ne peut pas savoir si une formule de la logique L est vraie ou non». Ou au contraire des résultats de décidabilité. C'est à dire que je donne un algorithme, parfois même je le code, qui résout un problème donné. En l'occurence j'ai principalement des «Est-ce que tel objet est définissable dans une logique».

Donc, non seulement, il faut que je dise quel est le rapport entre tous ça. Et le fait que «c'est les idées qui me sont passées par la tête, parfois soufflées pas mon directeur de thèse, et que j'ai réussi à démontrer» ça ne fait pas une vraie raison. Mais surtout, il faut que je trouve une notation cohérente pour TOUT ça. Et ça, c'est le 2ème point que je suis en train de réaliser.

J'ai pratiquement utilisé une notation différente par papier. Ce qui semble très bizarre à la relecture. D'abord car quand je reprend un papier des mois après je peux croire qu'une notation signifie ce qu'elle voulait dire dans un autre papier. Encore que la confusion soit rare. Mais surtout, j'ai l'envie d'unifier les notations. Or c'est une mauvaise idée, en effet j'ai un papier qui parle d'opérateurs, donc ma notation indique systématiquement quels sont les opérateurs que je m'autorise - en particulier, ça peut être «aucun opérateur». Mais dans tous les autres papiers où je n'ai jamais d'opérateurs, je ne vais pas mettre sans arrêt la notation «aucun opérateur», ça serait lourd inutilement.

Bon, là, c'est simple. Voyons un autre exemple. Mettons que je travaille en logique du premier ordre (abrégé en «FO») avec l'addition et un symbole R. Dans un cas je dis, «si R vérifie tel propriétés, alors on une formule f dans FO+,R qui vérifie tel propriété». Là, R se comporte comme un paramètre, en fait, c'est comme si on avait une infinité de théorèmes pour chaque valeur possible de R. Mais dans un autre cas, je dis «On a une formule f de FO+,R tel que R vérifie tel propriété si et seulement si f vérifie tel propriété». R est une variable comme une autre du théorème. La première différence, c'est que tout d'un coup, f est fixé, elle ne peut plus dépendre de R. Ça c'est habituel, c'est une inversion de l'ordre des quantificateurs. Mais on réalise qu'en fait, ce n'est pas «f» qui vérifie la propriété, «f» c'est une formule, et elle n'a pas de sens tant que R n'a pas de sens. Donc il faudrait dire: «On a une formule f de FO+,R telle que R vérifie tel propriété si et seulement si l'interprétation de f vérifie tel propriété», mais alors il faudrait aussi parler de l'interprétation de R par souci de cohérence. Et je me retrouve à dire «On a une formule f de FO+,R tel que l'interprétation de R vérifie tel propriété si et seulement si l'interprétation de f vérifie tel propriété». Et je le fais, car c'est le seul moyen d'être vraiment correct. Sauf que, voilà, si je veux être cohérent dans mes notations sur tous les papiers, mon premier résultat devrait être «si l'interprétation de R vérifie telle propriété, alors on une formule f dans FO+,R dont l'interprétation vérifie telle propriété». Et pour le coup, j'ai inutilement complexifié le premier résultat, car j'ai rajouté la distinction artificielle entre R et son interprétation. Artificielle, car je n'ai jamais tenté de distinguer + de son interprétation, qui est toujours l'addition.

En fait, le problème est que je dois faire comprendre que la signification de R peut varier énormément. R peut être considéré comme une variable, comme l'entrée d'un algorithme. Donc «si tu me donnes R, et qu'il vérifie tel propriété, alors je peux calculer ce truc» (ou au contraire, il est impossible de le calculer). Ça peut aussi être une valeur qu'on cherche à caractériser, comme dans «R est un nombre pair si et seulement si il existe un entier n tel que 2n=R».Et puis ça peut être une variable au sens mathématique, on cherche à caractériser les valeurs de R pour lesquelles une propriété est vraie. Voire simplement savoir s'il existe une telle valeur, auquel cas c'est comme si R était existentiellement quantifié. Mais ça serait lourd d'introduire explicitement R en tant que variable, et de le quantifier, car dans la plupart des papiers, cette notion n'est définie que pour les objets de premier ordre, et que ces objets n'ont pas le même statut que R.

Pour faire une comparaison, quand je dis «Cette logique est indécidable» je montre que pour toute machine de Turing, il existe une formule qui la simule. Mais je ne vais pas écrire «∃ f: formule» alors que f contiendra elle même des quantificateurs existentiels ∃, ça ne rendrait le tout que plus confus.

Je ne sais pas quoi conclure.