L'occurrence générale, dans les systèmes formels suffisamment expressifs, de l'existence d'énoncés vrais sur les structures visées qui ne sont pas démontrables au sein de ces systèmes ; englobe des résultats comme les théorèmes d'incomplétude de Gödel et d'autres limites de la formalisation.

Principe

Lorsqu'un système est suffisamment expressif pour encoder l'arithmétique de base, récursivement axiomatisable et cohérent, il ne peut être à la fois complet (prouver toute vérité) et efficacement axiomatisable ; l'autoréférence et la diagonalisation produisent des énoncés que le système ne peut prouver s'il est cohérent.

Démonstration

Le premier théorème d'incomplétude de Gödel construit, pour toute théorie cohérente et récursivement axiomatisable étendant une arithmétique minimale, une phrase qui affirme en substance «cette phrase n'est pas démontrable dans la théorie» et qui est donc vraie mais indémontrable dans cette théorie.

Mauvaise application

Prétendre que le phénomène d'incomplétude rend les mathématiques futiles ou que le raisonnement formel n'est pas fiable ; l'incomplétude ne limite que certains types de captures formelles et laisse de vastes domaines des mathématiques formellement gérables.

Conséquence

L'incomplétude impose de reconnaître les limites des systèmes formels uniques, motive l'étude de théories plus puissantes, de la métathéorie et des preuves de consistance relative, et légitime la sélection réfléchie d'axiomes supplémentaires si nécessaire.

Inversion

La complétude (au sens où une théorie prouve toute vérité d'une structure donnée) se rencontre dans des cadres plus faibles ou différents (p. ex. théories complètes, logiques propositionnelles décidables) ; les théorèmes de complétude pour la logique du premier ordre concernent l'entailment sémantique, pas la complétude des théories arithmétiques.

Limite

Le phénomène exige une puissance expressive suffisante (généralement la capacité de représenter les fonctions primitives récursives et de diagonaliser) ; il ne s'applique pas aux systèmes faibles dépourvus de cette expressivité ni aux sémantiques qui ne fixent pas de modèles intentionnels.

Tension sémantique

Il existe une tension entre l'incomplétude à la Gödel et les résultats de Tarski/Church/Complétude — entre les limites des théories formelles à capturer la vérité arithmétique et la complétude de la logique du premier ordre comme système de preuve pour l'entailment sémantique.

Synthèse

Le phénomène d'incomplétude identifie un écart inhérent entre vérité et démontrabilité formelle dans les théories suffisamment riches : des constructions autoréférentielles engendrent des phrases vraies mais indémontrables, poussant au développement d'axiomes plus forts et d'une compréhension métamathématique.