Blog personnel d'Arthur Milchior

En effet, parfois, je créé des formules logiques explicitement et j'ai besoin dans ma formule de rajouter «Vrai» ou «Faux». La solution la plus simple théoriquement, c'est de dire qu'en plus de «Non F», «F ou F», «il existe x tel que F» et «R(t,...,t)»^[1] je rajoute comme construction de base de ma logique «Vrai». Comme ça, pas de question à se poser, j'ai effectivement le droit de dire «Vrai» et «Faux» (enfin, «Non Vrai»). Le seul souci c'est que mes dizaines de preuves par induction sur les formules logiques devraient alors considérer la formule «Vrai». Ce qui est d'autant moins intéressant que dans la quasi-totalité des cas, ce traitement serait trivial.

L'autre solution est de dire que la formule atomique «Vrai» est implicitement supprimée dès qu'elle apparait. Ainsi «(Vrai et F)=(F et Vrai)=F», «(Vrai ou F)=(F ou Vrai)=Vrai», «(Non Non Vrai)=Vrai», «(Non Vrai et F)=(F et Non Vrai)=(Non Vrai)», «(Non Vrai ou F)=(F ou Non Vrai)=F». Ce qui fait que je n'ai plus besoin de regarder Vrai dans mes inductions... Sauf dans le cas de la formule atomique «Vrai», qui ne peut pas se simplifier. Ce qui amène à l'absurdité que chaque preuve serait une disjonction de la forme «Si F est Vrai, ou Non Vrai alors c'est trivial, sinon par induction sur F».

Pour éviter ça, une solution classique est de dire que «Vrai» est du sucre syntaxique pour «0=0», ou pour «x=x», ou pour «\forall x. x=x», selon qu'on ait accès aux constantes, à une variable libre x, ou aux quantifications respectivement. Seulement, il se trouve qu'il m'arrive de me restreindre à des logiques sans symbole de constantes(Parce que sur les réels, cela change l'expressivité), sans variable libre (quand je m'intéresse à la satisfiabilité de formules), ou sans quantificateurs (car ça simplifie énormément les preuves, et que j'ai la chance de considérer des logiques qui acceptent l'élimination des quantificateurs). Donc aucune de ces solutions ne fonctionnent pour moi.

Mais, le pire, de mon point de vue, c'est que aucune ne fonctionne uniquement à cause de la volonté d'avoir un formalisme unifié. En effet, je ne considère aucune logique sans quanticateurs, ni constantes, ni variables libres, pour la bonne raison que cette logique permettrait de ne rien exprimer.

Je fais de la théorie des modèles (finis), je tiens à vous dire que je n'envie pas ceux qui font de la théorie de la preuve, je crois qu'à côté d'eux, mais problèmes font figure de petit joueurs.