En logique mathématique, le théorème de complétude du calcul des prédicats du premier ordre établit 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.
Pourtant, des générations d'« hommes du nihil » se sont efforcées en vain de démontrer que « rien n'est », alors même que la vérité de cet énoncé crève les yeux et qu'il peut facilement s'exprimer en logique du premier ordre !
En dehors de l'homicide de soi-même — qui n'en est pas une à proprement parler — existe-t-il une démonstration formelle dérivant cet énoncé 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 ? Nous ne pouvons ici que poser la question.
(Włodzisław Szczur, Mathématique du néant)
