45 - Calculabilité

1 - Calculabilité

⇩ ⇧ ⤊

1 - La notion vague d'algorithme avant le 19e siècle

La notion d'algorithme est utilisée depuis très longtemps. Nous avons vu en 1er, que dès l'Antiquité, certains résultats et calculs pouvaient être déterminés en utilisant ces fameux algorithmes.

Pourtant la définition d'un algorithme est restée pendant très longtemps assez vague : une sorte de recette de cuisine pour certains, un ensemble d'instructions élémentaires pour d'autres...

Jusqu'au début du siècle dernier, bien peu de personnes soupçonnaient que l'on pourrait réellement préciser la notion d'algorithme.

2 - L'apparition de la logique mathématique

Avant de voir ce travail de formalisation de l'algorithme aboutir, il a fallu que la logique mathématique soit elle mếme formalisée à la fin du 19e siècle.

La logique mathématique est la branche des mathématiques qui s'intéresse aux mathématiques en tant que langage : la façon dont on formalise un énoncé mais aussi la façon dont on construit une démonstration.

Ce travail est le résultat d'un ensemble de recherches issues de plusieurs directions différentes :

• en 1847, George Boole publie les bases de l'algèbre qu'on nomme maintenant l'algèbre booléen (a ET b revenant à a.b, a OU b revenant à a+b comme vu en première approche en 1er...)
• en 1847, Auguste De Morgan publie ses propres travaux (dont les fameuses formules a+b = a . b..., rapidement vues en 1er également...)
• leurs travaux vont servir de base à ce qui va devenir une nouvelle branche des mathématiques : la logique mathématique. Gottlob Frege va clarifier et formaliser le raisonnement logique en 1879; notamment la logique des relations.
• les mathématiciens Gottlob Frege, Bertrand Arthur William Russell, Giuseppe Peano et David Hilbert vont travailler à donner une fondation axiomatique des mathématiques.
• en 1929, Kurt Gödel montre que tout ce qui est vrai dans le cadre d'une théorie mathématique est démontrable dans cette théorie. On pense alors qu'on va pouvoir un jour trouver la théorie mathématique ultime, celle qui permettra de tout démontrer//.
• en 1931, ce même Kurt Gödel va publier ses deux théorèmes d'incomplétude montrant que pour toute théorie mathématique permettant de faire des calculs basiques :
1. une théorie mathématique complète (une théorie qui permet de démontrer que toute proposition P est VRAIE ou FAUSSE) est nécessairement incohérente : dans cette théorie, on pourrait prouver qu'une proposition est VRAIE en utilisant une démonstration et FAUSSE en utilisant une autre démonstration !

Pour être utilisable, une théorie doit donc être incomplète : il existe certaines propositions P exprimées dans le cadre de la théorie qu'on ne peut ni démontrer (prouver que P est VRAIE), ni réfuter (prouver que P est FAUSSE) dans le cadre de cette théorie. Notez que cela ne veut pas dire que P est à la fois VRAIE et FAUSSE dans l'absolu mais la théorie ne permet pas en réalité de définir précisement la propriété sans ambiguïté ; on ne parviendra donc jamais à trouver une démonstration qui la prouve ou la réfute car il y a plusieurs interprétations possibles.

Il existe donc certaines propriétés pour laquelle on ne pourra jamais dire qu'elle soit toujours vraies ou toujours fausse. Imaginer une formule qui semble toujours fonctionner. Sur tous vos exemples préics, elle fonctionne. Mais, tant que vous n'avez pas démontré qu'elle est VRAI, vous ne pouvez pas avoir la certitude absolue qu'elle fonctionne toujours : il existe peut-être une valeur précise pour laquelle elle ne fonctionne pas.

Dans toute théorie mathématique incomplète, il existe donc des propositions qui sont indécidables.

2. Malheureusement, Gödel démontre également que déterminer si une théorie est incohérente est indécidable. Il n'existe donc pas d'algorithme permettant de savoir si une théorie est incohérente. C'est le fait de tomber, un jour, par hasard, sur une incohérence qui va lui donner un statut de théorie incohérente...

Tout ceci va permettre de redonner des bases stables et solides aux mathématiques : les mathématiciens ont pu se mettre d'accord sur un nombre limité des propriétés initiales (les axiomes) pour chaque théorie.

• Assez pour obtenir une théorie solide mais... incomplète.
• Pas trop pour espérer ne pas travailler sur une théorie qu'on découvrira un jour incohérente.

On pourrait le résumer en disant que penser tout savoir, c'est ne rien connaître...

Après ce petit détour par les théories mathématiques, revenons à l'informatique.

3 - La définition de l'algorithme et de la calculabilité

Le travail de formalisation de l'algorithme fut effectué en plusieurs étapes de 1931 à 1936 notamment par Alonzo Church, Stephen Kleene, Alan Turing et Kurt Godel.

• Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church invente le système formel du lambda-calcul (ou λ-calcul) qui fonde les concepts de fonction : cela formalise la notion de calcul.

Sans rentrer dans les détails, voici la façon dont on écrit la fonction successeur en λ-calcul :

λx.x+1 : cette codification veut dire que notre fonction attend de recevoir un argument x et qu'elle renvoie alors x+1. C'est bien la fonction successeur.

• La machine de Turing est un modèle abstrait du fonctionnement des appareils mécaniques de calcul créé par Alan Turing dans le but de définir précisement ce qu'est un algorithme et ce que représente la complexité d'un algorithme
• Les fonctions récursives sont également utilisées dans le cadre théorique de modèle de calcul par Kurt Godel, notamment dans ses théorèmes d'incomplétude.
• Stephen Kleene va démontrer l'équivalence entre les fonctions récursives et le λ-calcul, ainsi qu'entre les fonctions récursives et la machine de Turing. Cela va aboutir à la thèse de Church-Turing qui énonce (sans le démontrer) que toutes ces 3 méthodes de calcul "mécanique" (machine de Turing, λ-calcul et récursivité) sont équivalentes et peuvent toutes calculer les mêmes fonctions. Elles sont donc de même "puissance prédictive".

Calculabilité

La calculabilité est définie comme tout traitement

1. issu d'un système physique de calculs (qu'on assimilera à une machine de Turing pour préciser la notion)
2. répondant après un nombre d'étapes fini (et donc un temps fini)
3. en utilisant un jeu fini d'instructions

Le point 1 contenant le terme "système physique de calculs" posait problème dans le cadre d'une définition mathématique. C'est en partie pour cela que Turing a développé sa fameuse machine : de cette façon, il est parvenu à formaliser mathématiquement ce qu'est un système physique de calculs. On a déterminé le caractère universel de cette machine : elle peut émuler le comportement de n'importe quel autre système de calculs connus et est facilement représentable théoriquement.

La thèse de Church élargit encore la définition puisqu'elle affirme que les méthodes de calculs de la machine de Turing, du λ-calcul, de la récursivité ou de tout langage de programmation Turing-complet (comme Python) ont le même pouvoir de calcul : toutes ces méthodes sont équivalentes et permettent de faire les mêmes calculs.

Sans rentrer dans les détails de la démonstration, disons qu'il n'existe qu'un nombre limité d'algorithmes qui sont les combinaisons obtenues en prenant x mots dans l'alphabet du langage considéré contenant y symboles. Avec un langage comportant 1000 symboles et un programme de 400 caractères, on a 1000⁴⁰⁰ programmes différents (dont la plupart ne fonctionneront pas !). Un nombre fini, très grand, mais pas infini. Et donc, on ne pourra jamais calculer l'infinité des problèmes possibles à l'aide d'un programme fini.

Une fonction calculable est une fonction pour laquelle on aura toujours une réponse au bout d'un temps fini, quels que soient les paramètres (pourvu que les types et préconditions sur les paramètres soient vérifiés).

Une fonction non calculable est une fonction pour laquelle on aura parfois une réponse au bout d'un temps fini pour certains paramètres, et parfois aucune réponse car le calcul va provoquer une boucle infinie même avec des paramètres respectant les préconditions. Bien entendu, on ne peut pas savoir de façon certaine, en étudiant les paramètres d'entrées, si ces paramètres vont provoquer une boucle infinie. La seule manière certaine de savoir est de constater que la fonction réponde, et donc il faut la lancer... Au risque qu'elle ne réponde jamais... Ou qu'on perde patiente au bout d'un certain temps, et qu'on stoppe le calcul, alors que la réponse arrivait peut-être... Bref, elles sont incalculables car on ne peut pas savoir si, sur certains paramètres, elle ne va pas tourner en boucle.

On notera qu'en anglais la calculabilité se nomme computability ; on comprend bien le lien avec "computer".

2 - OPTIONNEL : Machine de Turing

⇩ ⇧ ⤊

Prenons quelques minutes pour voir ce qu'est cette fameuse machine de Turing même si aucune connaissance n'est attendue à ce sujet dans le programme. Cela vous permettra de comprendre ce qu'on entend par "machine physique".

Il s'agit donc d'une machine composée fondamentalement des éléments suivants :

• Un ruban (supposé infini s'il le faut) comportant des cases dans lequelles on peut écrire des valeurs issues d'un ensemble fini A de valeurs permises à définir. Je prendrais ici A = {∅, 0, 1} par exemple (A comme alphabet).
• Une tête de lecture se plaçant au dessus du ruban, pouvant lire le contenu d'une case et se déplacer à droite ou à gauche
• La tête de lecture possède une case-mémoire définissant son état. Elle peut prendre une valeur dans un ensemble fini T d'états. Par exemple T = {'init', 'travail', 'fini'}.
• Une table de transition (accessible depuis la tête) indiquant ce qu'on doit faire ensuite à partir de la lecture de la case du ruban et de l'état. Par exemple :

	∅	0	1
init	Etat ← init Case ← ∅ Vers Droite	Etat ← travail Case ← 0 Vers Droite	Etat ← travail Case ← 1 Vers Droite
travail	Etat ← fini Case ← 0 Vers Droite	Etat ← travail Case ← 0 Vers Droite	Etat ← travail Case ← 1 Vers Droite

Imaginons un ruban portant notamment des cases vides et une tête de lecture située sur l'une d'entre elles :

Notre ruban contient 010 au début, le reste étant constitué de cases vides.

Pour savoir ce qu'on doit faire, on doit aller lire la case (∅), l'état (init) et le tableau permettant d'en faire l'interprétation :

On applique en trois étapes les deux modifications et le déplacement :

La "nouvelle" configuration après la première séquence :

Situation semblable à la précédente : une lecture de case ∅ associée à init. Mêmes conséquences : on gére l'état, la valeur de la case puis on se déplace.

Nouvelle configuration après la deuxième séquence d'actions :

On obtient alors ces 3 actions élémentaires :

Nouvelle configuration après la troisième séquence d'actions :

Nouvelle configuration après la quatrième séquence d'actions :

Nouvelle configuration après la cinquième séquence d'actions :

Nouvelle configuration après la sixième séquence d'actions :

Et là, nous tombons sur un problème : le couple ('fini', ∅) n'est pas présent dans la table de transition : cette donné n'est pas interprétable comme une instruction !

Dans ce cas, la machine s'arrête.

On est parti de ce ruban :

Et on obtient ce ruban :

Le ruban de la machine est passée de 010 (soit 2 en décimal) à 0100 (soit 4 en décimal). Voilà ce que fait la table de transition de cette machine de Turing : elle multiplie par deux l'entier naturel encodé sur le ruban !

3 - Décidabilité

⇩ ⇧ ⤊

4 - Problème de l'arrêt

⇩ ⇧ ⤊

Vous allez découvrir aujourd'hui l'un des problèmes indécidables : le problême de l'arrêt d'un programme.

Le problème qu'on se pose est le suivant : peut-on créer un programme ou fonction arret() qui soit capable d'affirmer qu'un autre programme ou fonction quelconque p va s'arrêter un jour à coup sûr connaissant :

• le code-source du programme quelconque cs et
• les entrées e sur lesquelles p devra travailler.

La thèse de Church-Turing nous dit que cela revient à savoir si cette fonction Python peut exister :

Nous allons voir que ce problème de l'arrêt est indécidable : on ne peut pas créer un programme capable de détecter automatiquement si un autre programme dont on connait le code souce et les entrées va s'arrêter ou non.

Les mathématiciens Church et Turing ont prouvé que ce problème est indécidable avant même l'apparition réelle des ordinateurs.

Que faire avec notre énoncé "Existe-il un programme capable de détecter l'arrêt de n'importe quel autre programme ?" ?

Nous allons montrer que cela n'est pas possible en utilisant un raisonnement par l'absurde :

• Nous allons faire l'hypothèse qu'une telle fonction arret() existe
• Nous allons créer une nouvelle fonction inserer() valide et lui envoyant arret() en paramètre
• Nous allons montrer que l'existence de arret() mène à une incohérence. Cela permet de démontrer que l'hypothèse initiale de l'existence de arret() est fausse.

1 - Description de la fonction arret

Soit la fonction arret() suivante :

Notez bien que je ne donne pas le 'vrai code' : il n'existe pas mais ça n'a pas l'air inimaginable si ?

• Le paramètre p constitue donc le code de la fonction p.
• Le paramètre e contient les données qu'on voudrait confier à la fonction p si on l'exécute.

On imagine que la fonction arret() est capable d'analyser le code-source p et de dire si un vrai appel de type p(e) va répondre ou tourner à l'infini.

La seule chose à comprendre est donc que le code-source p n'est pas réellement exécuté : il s'agit juste d'analyse.

2 - Création d'une fonction inverser

Voici le code souce parfaitement valide de la fonction inverser() :

Aucune erreur. C"est bien une fonction correcte.

Notre fonction se nomme inverser() car :

• L05 : si arret détermine que f(f) s'arrête alors inverser(f) tourne en boucle .
• L06 : sinon, c'est que f(f) ne s'arrêtera pas et donc inverser(f) s'arrête.

Il n'y a donc aucun problème pour l'instant.

3 - Utilisation créant un paradoxe

Regardons maintenant ce qui va se passer si on fait l'appel suivant :

arret(inverser, inverser)

On se demande donc si la fonction inverser() s'arrête dans le cas d'un appel inverser(inverser). Imaginez un anti-virus qui analyse son propre code-source si cela vous choque. Vous verrez qu'il n'y a rien de génant en soi.

Souvenez-vous que nous avons fait l'hypothèse au départ que arret pouvait déterminer l'arrêt de n'importe quelle fonction.

Puisqu'on lance arret(inverser, inverser), lors de cet appel, cela revient mentalement à avoir quelque chose comme ceci :

Et c'est maintenant que nous allons observer la contradiction qui va mener à une absurdité.

Regardons ce qui se passe si arret(inverser, inverser) renvoie True, pour dire que inverser(inverser) va s'arrêter :

Cela revient à écrire :

Et c'est en ligne 6 ici qu'il y a un problème : la fonction arret affirme que cet appel inverser(inverser) s'arrête mais on voit bien qu'il va... boucler et ne pourra donc pas s'arrêter.

4 - Conclusion

1. Nous avons fait l'hypothèse de l'existence d'une fonction arret capable d'analyser le code de n'importe quel autre programme ou fonction pour savoir si il va s'arrêter et répondre sur l'entrée qu'on lui propose
2. l'utilisation de cette hypothèse associée à d'autres raisonnements corrects eux mène à une incohérence, un résultat absurde.
3. Cela veut donc dire que notre hypothèse de départ n'est pas bonne et qu'il n'existe pas de programme ou fonction arret capable d'analyser le code de n'importe quel autre programme ou fonction pour savoir si il va s'arrêter et répondre sur l'entrée qu'on lui propose.

5 - Fortement optionnel : indécidable ?

⇩ ⇧ ⤊

Les notions de décidabilité et d'indécidabilité sont loin d'être évidentes. Vous allez voir d'ailleurs qu'elles ne se limitent pas qu'aux algorithmes et à leurs limitations "physiques".

1 - Axiomes et théories mathématiques axiomatiques

Une théorie mathématique axiomatique est composée d'un ensemble d'axiomes, des propositions à la base de la théorie voulue. On les considère intrinséquement vraies dans le cadre de la théorie. Ce sont ces axiomes qui définissent l'objet abstrait sur laquelle la théorie travaille.

Important : les axiomes ne doivent pas être contradictoires entre eux bien entendu.

• La géométrie Euclidienne dispose de son jeu d'axiomes
• L'arithmétique dispose de son jeu d'axiomes
• La théorie des ensembles dispose de son jeu d'axiomes
• ...

2 - Construire des démonstrations à partir des axiomes

En associant ces axiomes à l'aide de la logique, on peut démontrer de nouvelles propriétés. D'où l'image des legos.

Une propriété vraie n'est donc jamais une invention : elle est présente depuis le début dans la théorie. Encore fallait-il savoir comment "l'assembler" pour la démontrer.

Un théorème est une propriété démontrée dont la portée d'utilisation est grande, ce qui justifie le fait qu'il soit reconnu dans le cadre d'une théorie donnéee. Comprendre par là que beaucoup de propriétés pourtant démontrées n'ont pas pour autant le statut de "théorèmes".

La démonstration d'une proposition P pourrait donc être représentée comme un Arbre dont

• les feuilles sont les axiomes et théorèmes (propriétés déjà démontrées et reconnues), et
• la racine est liée à la proposition P qu'on veut démontrer démontrer (aboutir à P est VRAI) ou réfuter (aboutir à NON P est VRAI).

Cet Arbre est un peu particulière puisque pour le réaliser on part des feuilles et on remonte vers la racine qui sera P si on démontre la propriété ou NON P si on la réfute. Les liens de parenté sont établis en utilisant les règles de la logique que nous avons vu (ET, OU, NON, IMPLIQUE...)

Cela devrait vous faire penser à nos algorithmes : des associations d'instructions aboutissant à une réponse.

3 -Le choix des axiomes

Le choix des axiomes à prendre en compte pour rendre chacune des théories "efficaces" est un enjeu majeur.

Une fois les bases de la logique mathématique posées par les travaux de Bool et De Morgan, Frege va clarifier et formaliser le raisonnement logique en 1879 et va dégager trois caractéristiques qu'une théorie mathématique devrait avoir (notez que j'utilise le conditionnel) :

1. cohérence : impossibilité de démontrer une proposition et son contraire
2. complétude : à l'intérieur de la théorie, tout énoncé A est
• soit démontrable (A est VRAI),
• soit réfutable (not A est VRAI)
3. décidabilité : il existe une procédure de décision permettant de tester tout énoncé de la théorie.

Tout ceci va aboutir à une profonde refondation des mathématiques par les théoriciens de l'époque : la formalisation de la logique mathématique et l'apparition des théories axiomatiques. Grande réussite des mathématiques : son auto-réflexivité lui permet d'étudier des objets qui sont eux-mêmes... les théories mathématiques.

De nombreux théoriciens (dont Hilbert) vont justement tenter de trouver quels axiomes choisir pour chaque théorie de façon à éviter deux problèmes :

• Si on sélectionne trop peu d'axiomes comme fondation d'une théorie, on peut aboutir à des situations où certaines propositions (qui pourtant sont bien VRAIES ou FAUSSES) ne sont ni démontrables, ni réfutables : la théorie construite est incompléte : on manque de "briques" pour construire certains raisonnements.

On peut ainsi trouver des énoncés pour lequels :

• alors que la proposition P est vraie, on ne parviendra jamais à le démontrer... Pour vous donner une image de ce cas, imaginez le théorème de Pythagore en version conjoncture et sans que jamais on ne parvienne à la démontrer. Dans ce cas, il est vrai mais on ne pourra pas lui faire ABSOLUMENT confiance. Tous les exemples montrent qu'on obtient le bon résultat, mais on ne parvient pas à le démontrer. C'est donc un peu l'équivalent d'une fonction qu'on a créé, qui a l'air de fonctionner mais dont on ne parvient pas à prouver la correction.
• alors que la proposition P est fausse, on ne parviendra pas à la réfuter.


Si on revient à l'image de l'Arbre, cela veut dire qu'on ne parviendra jamais à atteindre P ou NON P en partant des axiomes et théorèmes (propositions démontrées) de la théorie. La théorie ne peut donc pas trancher (ce qui ne veut pas dire que la propriété P n'est pas soit VRAI soit FAUX)

• Si on sélectionne trop d'axiomes comme fondation d'une théorie, il existe des propositions P pour lesquelles on parvient à montrer P avec une démonstration et à réfuter P avec une autre démonstration : la théorie construite est incohérente. Là, c'est l'inverse du coup précédent : on a trop de briques et on finit par pouvoir bâtir des raisonnements contradictoires.

On pourrait ainsi trouver deux arbres de démonstration, l'un menant à P et l'autre menant à NON P.

Situation embarrassante...

Il y a toujours des énoncés qui sont uniquement VRAI ou uniquement FAUX. Mais, il existe dans ces théories des énoncés dont on peut démontrer qu'ils sont VRAI en suivant un raisonnement et FAUX en suivant un autre raisonnement. Bref, c'est une théorie dans laquelle il est dangereux de faire confiance à ce qu'on démontre.

A partir du moment où ceci a été clairement établi, plusieurs mathématiciens ont tenté pendant des années d'aboutir au parfait choix d'axiomes, un choix qui permettrait d'aboutir à ceci :

On parle de tiers exclus : soit c'est VRAI et démontrable, soit c'est FAUX et réfutable.

Trouver cette théorie parfaite permettrait de pouvoir répondre à n'importe quel énoncé portant sur l'objet d'études de la théorie. Pourvu qu'on parvienne comment la démontrer ou la réfuter. Mais savoir qu'une démonstration ou une réfutation existe serait déjà confortable : on sait au moins qu'on travaille à trouver quelque chose qui existe.

4 - La réponse de Kurt Gödel

Un jeune mathématicien autrichien (naturalisé américain après sa suite du régime nazi) va alors parvenir à démontrer en 1931 deux théorèmes importants de la logique mathématique.

Le premier théorème d'incomplétude établit qu'une théorie suffisante pour y démontrer les théorèmes de base de l'arithmétique est nécessairement incomplète : certains énoncés seront nécessairement indécidables dans cette théorie. Rappelons que cela signifie simplement qu'on ne pourra jamais les démontrer ou les réfuter dans le cadre de cette théorie.

Le second théorème d'incomplétude va lui établir qu'une théorie cohérente ne peut pas démontrer sa propre cohérence.

Notez bien que cela n'empêche pas les mathématiciens de dormir : ne faites pas dire à ces théorèmes plus qu'ils ne le font. Cela veut juste dire

• qu'il existera toujours des énoncés indécidables dans une théorie cohérente
• qu'on ne peut pas démontrer qu'une théorie est cohérente même si elle l'est : cela fait partie des énoncés... indécidables de la théorie.

Si les axiomes utilisés pour batir les théories reconnues actuelles menaient à des théories incohérentes, quelqu'un aurait bien réussi à trouver un cas problématique. Et même dans ce cas, il "suffirait" sans doute de redefinir un système d'axiomes un peu plus restreint. Certains choses seraient à revoir, mais pas tout. C'est ce qui s'est passé avec la première version de la théorie des ensembles. Après ajustement, elle n'en est que plus solide.

L'informatique théorique étant l'étude des fondements logiques et mathématiques de l'informatique, on va bien entendu retrouver les mêmes conséquences.

Néanmoins, souvenez-vous de ce qu'on vous a raconté sur les algorithmes : ils ne sont pas conçu pour résoudre un énoncé unique mais toute une classe d'énoncés similaires.

On le résumera en disant qu'un algorithme est concu pour résoudre une classe de problèmes et pas une seule instance du problème.

Et certains problèmes ne seront pas résolvables par un algorithme. On dira que ces problèmes sont indécidables de façon absolue.

5 - L'algorithme de démonstration ultime ?

Nous avons vu qu'une démonstration est en quelque sorte un Arbre utilisant les axiomes d'une théorie et de la logique.

Vous connaissez certainement l'histoire du singe qu'on place devant un clavier. En le laissant tapant ce qu'il veut pendant un temps infini, on pourrait obtenir une copie de n'importe quelle oeuvre.

Nous pourrions faire de même avec les démonstrations : faire tourner un programme qui teste un par un tous les Arbres de démonstration possibles à partir d'un certain ensemble d'axiomes jusqu'à démontrer ou réfuter n'importe quelle proposition P qu'on lui fournit en ENTREE. Si, pendant le parcours des raisonnements possibles, nous obtenons

• un Arbre dont la racine est P, nous aurons démontré la proposition P. L'algorithme pourrait renvoyer True.
• un Arbre dont la racine est NON P, nous aurons réfuté la proposition P. L'algorithme pourrait renvoyer False.

evaluer_une_proposition(proposition, axiomes:list) -> bool

Malheureusement, dans le cadre d'une théorie suffisamment élaborée, nous ne pourrons jamais prouver la correction de cet algorithme à cause du premier théorème d'incomplétude : certaines propriétés font partie des propriétés indécidables : il est donc certain que l'algorithme va parfois établir des Arbres de démonstration sans jamais tomber ni sur P, ni sur NON P pour la bonne raison de cette proposition précise n'est ni démontrable, ni réfutable !

Notre programme pourrait donc tomber par hasard sur certaines démonstrations, mais ne peut pas démontrer ou réfuter n'importe quelle proposition fournie en ENTREE : il n'est donc pas CORRECT

Il s'agit donc d'un problème indécidable car même en changeant de théorie cohérente, il y aura toujours des propositions indécidables.

6 - FAQ

⇩ ⇧ ⤊

Rappel : Preuve de terminaison

Rappel : Preuve de correction et invariant