Théorème de définissabilité de Beth

Le théorème de définissabilité de Beth est vraie en logique du premier ordre, mais donnons une explication informelle avec un exemple de géométrie. Supposons que l'on dispose d'une théorie T sur les formes géométriques et soit T⁺. une théorie qui introduit le nouveau concept carré. Le fait que le concept carré soit explicitement définissable dans T⁺ signifie qu'il existe une définition avec une formule logique, par exemple, "rectangle et losange", c'est-à-dire que dans théorie T⁺, on a carré ↔ (rectangle et losange) valide. Autrement dit, la notion d'être un carré est définie explicitement comme être à la fois un rectangle et être un losange. Le théorème de définissabilité implique que le fait d'être explicitement définissable avec une formule est équivalent au fait d'être implicitement définissable dans le sens suivant :

• Dans tout modèle (i.e. pour toute forme géométrique), il n'y a qu'une façon de donner une interprétation à carré si ce modèle est un modèle de T⁺.

Soit L un langage du premier ordre et R un symbole de relation qui n'est pas dans L. Soit L⁺ le langage qui étend L en incluant le symbole R. Soit T⁺ une théorie sur L⁺. On dit que :

• R est T⁺-explicitement définissable s'il existe une formule φ(x⃗) telle que la formule R(x) ↔ φ(x⃗) est T⁺-valide.
• R est T⁺-implicitement définissable si pour tout L-modèle M, pour toute interprétations possibles I, J de R, si le modèle M étendu avec I pour R et le modèle M étendu avec J pour R sont tous les deux des modèles de T⁺, alors I = J.

Le théorème de définissabilité de Beth dit alors que R est T⁺-explicitement définissable si et seulement si R est T⁺-implicitement définissable.

Considérons le langage L avec +, ., =, 0, 1. Considérons le symbole de relation ≤ qui n'est pas dans L et soit L⁺ le langage qui étend L en incluant le symbole ≤. Soit T⁺ la théorie des corps clos sur L⁺. On a :

• ≤ est T⁺-explicitement définissable : en effet, la formule (x≤y) ↔ (∃z y = x + z²) est T⁺-valide.
• ≤ est T⁺-implicitement définissable : en effet, dans tout L-modèle M, si on cherche à interpréter ≤ de façon satisfaire T⁺, l'interprétation de ≤ est défini de manière unique.

Le théorème est également vrai pour la logique propositionnelle. Une variable propositionnelle qui est explicitement définissable s'appelle une porte. Le calcul des portes pour utile pour faire du préprocessing pour calculer le nombre de valuations d'une formule booléenne. Le théorème de définissabilité de Beth intervient dans un algorithme de preprocessing[2].