Un ensemble de phrases formulées en logique du premier ordre sur une signature fixée, fermé sous conséquence logique, qui spécifie des propriétés devant être vérifiées dans les structures de cette signature.

Principe

La théorie du premier ordre organise l'information mathématique syntaxiquement : des axiomes et leurs conséquences en logique du premier ordre déterminent la classe des modèles ; la fermeture sous conséquence logique garantit que la théorie contient toute phrase déductible de ses axiomes.

Démonstration

Les axiomes de la théorie des groupes (associativité, élément neutre, inverses) forment une théorie du premier ordre dans le langage muni d'un symbole binaire · et d'un symbole constant e ; toute structure interprétant · et e qui satisfait ces axiomes est un modèle de la théorie, et toute phrase dérivable des axiomes de groupe appartient à la théorie.

Mauvaise application

Tenter d'exprimer des propriétés essentiellement du second ordre, comme « le domaine est fini » ou « tout sous-ensemble admet un maximum », par une théorie du premier ordre et s'attendre à ce qu'elles y soient complètement capturées ; ces propriétés ne sont pas préservées par l'équivalence élémentaire et ne peuvent donc pas être fixées par des axiomes du premier ordre.

Conséquence

À partir d'une théorie du premier ordre, les méthodes de la théorie des modèles s'appliquent : on étudie les modèles, les extensions élémentaires, la complétude ou l'incomplétude de la théorie, et l'on utilise le compactness et les phénomènes de Löwenheim–Skolem pour obtenir des résultats d'existence et de cardinalité des modèles.

Inversion

Vu en sens inverse, au lieu d'un ensemble déductivement clos de phrases, on peut partir d'une classe de structures et considérer l'ensemble de toutes les phrases du premier ordre vraies dans chaque membre ; l'inversion met en évidence le point de vue sémantique (théorie comme théorie commune d'une classe) plutôt que le point de vue syntaxique.

Limite

Ne concerne que les phrases de la logique du premier ordre dans une signature fixe ; exclut la quantification d'ordre supérieur, les axiomes catégoriques du second ordre et les contraintes sémantiques qui ne peuvent être exprimées ou imposées par des phrases du premier ordre.

Tension sémantique

Tension entre la théorie en tant qu'objet purement syntaxique, déductivement clos, et la classe sémantique de ses modèles ; deux théories différentes peuvent avoir la même classe de modèles (au sens de l'équivalence élémentaire), et une même théorie peut admettre des modèles non isomorphes satisfaisant toutes ses phrases.

Synthèse

Une théorie du premier ordre est l'ensemble déductivement clos de phrases du premier ordre dans une signature donnée qui décrit une collection de structures en spécifiant ce que tous les modèles doivent satisfaire ; elle relie les axiomes syntaxiques aux classes sémantiques de modèles dans les limites de l'expressivité du premier ordre.