ATLAS
Ouvrir dans l'atlas →AxiomeLogique du premier ordre
Le cadre de la logique
La logique est placée sous la théorie des ensembles, alors que sa sémantique emploie des ensembles : ce n'est pas un cercle, mais un échelonnement. La syntaxe, qui ne manipule que des mots finis, n'exige qu'une arithmétique élémentaire des suites finies. La sémantique, elle, emploie des ensembles intuitifs. Une fois posée sur cette base, on peut tout recoder à l'intérieur. Gödel, pour démontrer l'incomplétude, fait un recodage du même genre dans l'arithmétique : les formules et les démonstrations y deviennent des entiers.
La logique étudie des mots, suites finies de symboles pris dans un alphabet, et des structures qui leur donnent un sens. Pour en parler, on s'autorise les notions du raisonnement mathématique ordinaire : ensembles, applications, entiers naturels, récurrence, ensembles finis et dénombrables, pris dans leur sens intuitif. C'est la métathéorie.
Les notions de la métathéorie recevront plus loin une définition rigoureuse dans : applications au nœud Relations, fonctions, entiers au nœud ℕ. Elles ne sont utilisées ici que dans leur sens intuitif, et jamais comme objets de la théorie étudiée.
La métathéorie n'emploie aucune forme de l'axiome du choix, sauf en un endroit, signalé par ⋆ : le lemme de Lindenbaum pour une signature non dénombrable, où l'on admet un principe de maximalité, qui est le lemme de Zorn pour l'inclusion. Les théorèmes de complétude et de compacité en dépendent pour de telles signatures, et pour elles seulement.