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

Résumé

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.

Source officielle

https://fr.wikipedia.org/wiki/Théorème_de_complétude_de_Gödel

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (59)

Logique mathématique

La logique mathématique ou métamathématique est une discipline des mathématiques introduite à la fin du , qui s'est donné comme objet l'étude des mathématiques en tant que langage. Les objets fondamentaux de la logique mathématique sont les formules représentant les énoncés mathématiques, les dérivations ou démonstrations formelles représentant les raisonnements mathématiques et les sémantiques ou modèles ou interprétations dans des structures qui donnent un « sens » mathématique générique aux formules (et parfois même aux démonstrations) comme certains invariants : par exemple l'interprétation des formules du calcul des prédicats permet de leur affecter une valeur de vérité'.

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

Axiomes de Peano

vignette|Giuseppe Peano En mathématiques, les axiomes de Peano sont des axiomes pour l'arithmétique proposés initialement à la fin du par Giuseppe Peano, et qui connaissent aujourd'hui plusieurs présentations qui ne sont pas équivalentes, suivant la théorie sous-jacente, théorie des ensembles, logique du second ordre ou d'ordre supérieur, ou logique du premier ordre. Richard Dedekind avait proposé une formalisation assez proche, sous une forme non axiomatique.

Afficher plus

Cours associés (10)

MATH-483: Gödel and recursivity

Gödel incompleteness theorems and mathematical foundations of computer science

MATH-318: Set theory

Set Theory as a foundational system for mathematics. ZF, ZFC and ZF with atoms. Relative consistency of the Axiom of Choice, the Continuum Hypothesis, the reals as a countable union of countable sets,

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

Afficher plus

Séances de cours associées (78)

Comportement asymptotique de Gradient Vestimer

Couvre le comportement asymptotique de gradient vestimer et la conclusion de Peano, soulignant l'importance d'un comportement public spécialisé.

Bien-fondé et exhaustivité d'un système de preuve proposé

Explore l'importance de la solidité et de l'exhaustivité dans un système de preuve propositionnelle.

Protocoles de délégation quantique

Couvre les protocoles classiques de vérification hamiltonienne simple qubit et de délégation quantique.

Afficher plus