Décider la validité d'une formule

[invite855de8be]

Bonjour,

Il n'existe pas d'algorithme pour décider de la validité d'une formule dans le calcul des prédicats. (alors qu'il en existe pour le calcul propositionnel : il suffit de tester toutes les valuations)

Comment peut-on le prouver svp ?
-----

[Médiat]

Bonjour,

D'abord, il faut faire attention, le calcul des prédicats est décidable dans certains cas (langage restreint à des prédicats unaire (en plus de l'égalité), par exemple).

Pour le cas général, il faut regarder les travaux de Church et de Turing, ce dernier ayant montrer que dans certains cas (langage de l'arithmétique, par exemple), le problème de la décidabilité se ramène au problème de l'arrêt d'une machine de Turing...

[invite855de8be]

Ah merci déjà pour cette précision, maintenant que vous le dites je suis tout à fait d'accord mais je ne l'avais pas à l'esprit.

Auriez-vous un lien de la preuve que dans le langage de l'arithmétique, il n'y a pas d'algorithme pour décider de la validité d'une formule svp ?

[edit] J'ai trouvé la citation suivante :

Pour montrer l'indécidabilité de l'arithmétique, l'argumentation d'Alan Turing est la suivante. Supposons que nous ayons un algorithme de décision pour l'arithmétique de Peano. La question de savoir si une machine de Turing donnée s'arrête ou non, peut être formulée comme un énoncé du premier ordre (on utilise les méthodes développées par Gödel), lequel serait alors résolu par l'algorithme de décision. Mais Turing avait prouvé précédemment qu'il n'y a pas d'algorithme général pour décider de l'arrêt d'une machine de Turing.

Je vais m'en contenter.