title: Théorème de définissabilité de Beth
text: # Théorème de définissabilité de Beth
  
  En logique mathématique, le théorème de définissabilité de Beth (d'après Evert Willem Beth) établit que deux notions de définissabilité sont équivalentes : il s'agit des notions d'être implicitement ou explicitement définissable dans une théorie du premier ordre.
  
  ## Explication informelle
  
  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^+.$
  
  ## Énoncé
  
  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.
  
  ## Exemple
  
  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^2)$ 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.
  
  ## Application
  
  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.
  
  