Théorème de complétude de Gödel

En logique mathématique, le théorème de complétude du calcul des prédicats du premier ordre dresse une correspondance entre la sémantique et les démonstrations d'un système de déduction en logique du premier ordre. En termes intuitifs le théorème de complétude construit un pont entre vérité et démontrabilité formelle : tout énoncé vrai est démontrable. Plus précisément le théorème de complétude affirme que si un énoncé est conséquence sémantique d'une théorie que l'on peut décrire dans le formalisme du calcul des prédicats du premier ordre, c'est-à-dire qu'il est vrai dans tous les modèles de cette théorie, alors il est conséquence syntaxique de cette théorie : il existe une démonstration formelle qui déduit cet énoncé à partir des axiomes de la théorie en utilisant les règles d'un système de déduction comme la déduction naturelle, le calcul des séquents ou un système à la Hilbert. Le théorème de complétude de la logique du premier ordre a été démontré pour la première fois par Kurt Gödel en 1929 dans sa thèse de doctorat, sur la complétude du calcul logique. Leon Henkin a ensuite simplifié la démonstration dans sa thèse The Completeness of Formal Systems (la complétude des systèmes formels) publiée en 1949. La preuve de Henkin a ensuite été simplifiée à son tour par Gisbert Hasenjaeger en 1953. Le théorème de complétude est un méta-théorème qui relie deux concepts : celui de conséquence sémantique et de conséquence syntaxique dans un système de déduction logique. Le premier concept à définir est donc celui de déduction logique, il dit qu'on peut donner un nombre fini d’axiomes, de schémas d’axiomes ou de règles d'inférence pour décrire ou formaliser la partie purement logique de la déduction, autrement dit toutes les démonstrations qui sont décrites en des étapes élémentaires de raisonnement sont obtenues à partir de ces principes. La validité logique d’un axiome, d'un schéma d'axiomes ou d'une règle d'inférence est garantie par des modèles. Ainsi, une règle de déduction est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion.