Lazi

Traduire par une recherche de preuve

Contexte

Avec les règles de déduction actuelles il n'est pas possible de raisonner par tiers exclu sur une condition comme "le calcul se finit".

Question

Est-il possible de traduire un tiers exclu du premier ordre en cherchant la preuve de la finitude ou non du calcul ?

Étude

Le problème de l'arrêt

La solution étudiée dans cette étude est en rapport avec le problème de l'arrêt: existe-t-il une fonction calculable qui peut déterminer pour tout calcul si il s'arrête ou non ? Il est sensé existé une preuve que cette fonction ne peut exister. Si cette fonction de calcul d'arrêt n'existait pas, alors on ne pourrait effectuer une recherche par preuve, puisque cette fonction de recherche par preuve résoud le problème de l'arrêt.

Mais la preuve fournie semble avoir un problème, voir les articles:

  • "Problems with the Halting Problem" Eric C.R. Hehner
  • "Halting misconceived?" de Bill Stoddart
Je trouve le problème mieux expliqué dans le deuxième article, je le comprend comme ceci: la preuve construit une représentation de formule infinie car elle se contient elle-même. Hors une représentation de formule ne peut être infinie.

Une fonction résolvant le problème de l'arrêt ?

Soit prooveHalt la fonction qui prend en argument une représentation de formule et qui explore toutes les preuves possibles, en recherchant une preuve ayant pour conclusion soit que le calcul de la formule s'arrête, soit que le calcul de la formule ne s'arrête pas.

Si une fonction résolvant le problème de l'arrêt existe

Alors cela implique que l'on peut définir une fonction "calculable" qui retourne 0b ou 1b. C'est important pour pouvoir transformer les fonctions qui peuvent boucler en fonctions qui ne bouclent pas, et donc pouvoir faire des raisonnement par tier exclu sur des expressions utilisant des fonctions comme "isList".

Bestiaire de calculs dont on peut tester la calculabilité:

  • calcul cherchant une preuve d'un théorème, qui retourne 1b si elle la trouve et bouclant si elle ne la trouve pas. Cela implique que la fonction prooveHlalt peut déduire pour toute théorème s'il est vrai ou s'il ne l'est pas (qu'il soit indécidable ou faux).
  • calcul cherche un nombre premier valant 3 modulo 4 et qui est somme de carrés d'entiers. Pour prouver que ce calcul est infini, il faut démontrer le théorème des deux carrés de Fermat

On voit que le problème de l'arrêt pousse à résoudre des problèmes très généraux, et donc la seule manière simple de définir prooveHalt est d'explorer toutes les démonstrations.

Comment exprimer qu'un calcul est infini ?

On ne peut pas l'exprimer à l'ordre zéro, car il faut "réaliser" le calcul pour vérifier qu'il est infini, et donc on exécute un calcul infini.

On peut l'exprimer à l'ordre 1 avec un "∀" et un "⊢" : pour tout x, si x est une liste, la longueur du calcul est plus grande que la longueur de x.

Pour toute formule x, proveHalt x est calculable

Raisonnons par l'absurde et supposons que pour une certaine formule x, proveHalt ne s'arrête pas

Cela implique que la question "le calcul de x s'arrête" est indécidable (voir la sous-étude). Mais si on calcul x et que le calcul s'arrête alors on a une preuve que le calcul de x est fini, hors il n'existe pas de telle preuve, donc le calcul de x ne peut s'arrêter, donc le calcul de x est infini. Mais alors on vient de prouver que le calcul de x est infini, ce qui est absurde puisqu'il n'y a pas de preuve que le calcul de x est infini. Donc proveHalt s'arrête toujours. Donc pour toute formule on peut prouver qu'elle s'arrête ou non.

Mais est-ce en contradiction avec le théorème de Rice ?

Voir le théorème de Rice ? Ce théorème semble utiliser le théorème de l'arrêt qui semble avoir des problèmes (voir plus haut "Le problème de l'arrêt").

Les règles utilisé par le raisonnement

Remarquons que le raisonnement ci-dessus utilise des règles de haut niveau:

  • tiers exclu sur la finitude du calclul de "proveHalt x"

Extension à la complétude ?

Utilisons le résultat ci-dessus que "Pour toute formule x, proveHalt x est calculable" et cherchons à l'étendre.

Soit x une formule, soit f un calcul qui énumère toutes les preuves et s'arrête ssi il rencontre une preuve de x. Comme proveHalt f est calculable, cela implique qu'il est décidable que f soit calculable, or f calculable signifie que x est prouvé, donc il est décidable que x soit prouvé, donc ont peut trouver une preuve de soit:

  • x est prouvé
  • x n'est pas prouvé (il peut être indécidable ou faux).

Soit x une formule, soit f un calcul qui énumère toutes les preuves et s'arrête s'il rencontre une preuve de x ou de la négation de x. Donc f est calculable est équivalent à x est décidable. Hors comme proveHalt x est calculable on déduit que la décidabilité de x est décidable.

Utilisation dans le tiers exclu ?

Expression "∀ x | f x "

Supposons que l'on ait montré que f x est décidable. Soit g la fonction qui parcourt toutes les formules, et pour chacunne d'elle x recherche si f x est faux et s'arrête dans ce cas. Comme f x est décidable, pour chaque x la recherche si f x est faux peut être faite en un temps fini. Comme prooveHalt g est calculable, ∀ x | f x

est décidable. Donc on peut utiliser le tiers exclu car on peut traduire...

Réponse

@todo