Théorie

Logique du premier ordre ⋆

Un langage du premier ordre comporte des variables, des symboles de relation et de fonction, les connecteurs $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$ et les quantificateurs $\forall, \exists$, qui portent sur les éléments et jamais sur les parties ni sur les propriétés.

Une démonstration à partir d'une théorie $T$ est une suite finie de formules dont chacune est un axiome logique, un axiome de $T$, ou se déduit des précédentes par une règle d'inférence. Le théorème de complétude de Gödel (1929) affirme qu'une formule est démontrable dans $T$ si et seulement si elle est vraie dans tous les modèles de $T$.