##  [Généralisation Universelle](/fr/node/60940) 

 Définition

Règle d'inférence formelle en logique du premier ordre qui permet de déduire une formule universelle ∀x φ(x) lorsqu'on a dérivé φ(x) dans les conditions où x est arbitraire et ne dépend d'aucune hypothèse portant sur cet individu particulier.

 

 

 

 

 

 





## Principe

Principe

Si une formule est démontrée pour un élément choisi arbitrairement — dont le nom n'apparaît dans aucune hypothèse non libérée — alors elle vaut pour tout élément ; l'instance arbitraire légitime l'introduction du quantificateur universel.

 

 

 

 

 





## Démonstration

Démonstration

Supposons que, sans aucune prémisse mentionnant le symbole a, on démontre P(a) en n'utilisant que des règles qui ne font aucune hypothèse spécifique sur a. Par généralisation universelle on peut en déduire ∀x P(x). Par exemple, à partir d'une preuve montrant que 'a est pair' traitant a comme arbitraire, on peut inférer 'tout entier est pair' seulement si la condition d'arbitrarité est respectée.

 

 

 

 

## Mauvaise application

Mauvaise application

Appliquer la règle lorsque le symbole témoin a été introduit par une hypothèse non libérée ou dépend de prémisses le concernant (par exemple déduire P(a) à partir de 'a = 0' puis conclure ∀x P(x)) conduit à une généralisation illicite.

 

 

 

 

 





## Conséquence

Conséquence

Bien appliquée, elle permet d'abstraire d'un cas représentatif vers une loi générale, autorisant la formation de théorèmes universels et l'introduction du quantificateur dans les démonstrations.

 

 

 

 

## Inversion

Inversion

Le mouvement dual est l'instanciation universelle : de ∀x φ(x) on déduit φ(t) pour un terme particulier t. Généralisation et instanciation universelles relient les directions générale et particulière du quantificateur.

 

 

 

 

 





## Limite

Limite

Exige que la variable (ou constante témoin) ne dépende pas d'hypothèses non libérées et n'apparaisse pas dans des prémisses qui la contraignent. Dans certains cadres modaux, constructifs ou typés, des restrictions supplémentaires sont nécessaires pour éviter des généralisations non valides.

 

 

 

 

 





## Tension sémantique

Tension sémantique

Tension entre la règle syntaxique d'introduction de ∀ dans une preuve et la notion sémantique d'« être vrai pour tous les éléments d'un modèle » ; une généralisation syntaxique peut être bloquée par des contraintes de formation de preuve même si la formule est sémantiquement valide.

 

 

 

 

 





## Synthèse

Synthèse

La Généralisation Universelle est la règle de preuve qui transforme une dérivation portant sur un représentant arbitraire, indépendant des hypothèses, en une assertion universelle, sous conditions de nouveauté et d'indépendance.