Le théorème de Herbrand établit un lien entre la logique du premier ordre et la logique propositionnelle — qui peut être vue, selon l'homme du nihil, comme la logique d'ordre zéro.
La validité (ou prouvabilité) d'une formule du premier ordre se ramène à la validité (ou prouvabilité) d'un ensemble fini de formules propositionnelles.
Alors qu'il est possible de déterminer si une formule propositionnelle — par exemple la formule de Pascal « le Moi est haïssable » — est démontrable ou pas, on sait, depuis les travaux de Gödel, Tarski, Church, Turing et tutti quanti, que la même question pour les formules du premier ordre est indécidable. Le théorème de Herbrand montre qu'elle est cependant semi-décidable : il existe une procédure qui résout partiellement la question en répondant « non » à tout coup.
(Włodzisław Szczur, Mathématique du néant)
Aucun commentaire:
Enregistrer un commentaire