Variable de prédicat

En logique mathématique , une variable prédicat est une lettre prédicat qui fonctionne comme un « espace réservé » pour une relation (entre des termes), mais à laquelle aucune relation (ou signification) particulière n'a été spécifiquement attribuée. Les symboles courants pour désigner les variables prédicatives comprennent les lettres romaines majuscules telles que , et , ou les lettres romaines minuscules, par exemple . En logique du premier ordre , elles peuvent être plus correctement appelées variables métalinguistiques . En logique d'ordre supérieur , les variables prédicatives correspondent à des variables propositionnelles qui peuvent représenter des formules bien formées de la même logique, et ces variables peuvent être quantifiées au moyen de quantificateurs (au moins) du second ordre .

Les variables prédicatives doivent être distinguées des constantes prédicatives, qui pourraient être représentées soit par un ensemble différent (exclusif) de lettres prédicatives, soit par leurs propres symboles qui ont réellement leur propre signification spécifique dans leur domaine de discours : par exemple .

Si des lettres sont utilisées à la fois pour les constantes de prédicat et les variables de prédicat, il doit alors y avoir un moyen de les distinguer. Une possibilité est d'utiliser les lettres W , X , Y , Z pour représenter les variables de prédicat et les lettres A , B , C ,..., U , V pour représenter les constantes de prédicat. Si ces lettres ne suffisent pas, des indices numériques peuvent être ajoutés après la lettre en question (comme dans X ₁ , X ₂ , X ₃ ).

Une autre option consiste à utiliser des lettres minuscules grecques pour représenter de tels prédicats métavariables. Ces lettres pourraient alors être utilisées pour représenter des formules bien formées (wff) entières du calcul des prédicats : tous les termes variables libres de la wff pourraient être incorporés comme termes du prédicat en lettres grecques. C'est la première étape vers la création d'une logique d'ordre supérieur.

Si les variables de prédicats ne sont pas définies comme appartenant au vocabulaire du calcul des prédicats, alors elles sont des métavariables de prédicats , tandis que les autres prédicats sont simplement appelés « lettres de prédicats ». Les métavariables sont donc censées être utilisées pour coder les schémas d'axiomes et les schémas de théorèmes (dérivés des schémas d'axiomes).

Que les « lettres prédicatives » soient des constantes ou des variables est un point subtil : ce ne sont pas des constantes au même sens que les constantes prédicatives ou que les constantes numériques.

Si les « variables de prédicat » ne peuvent être liées qu'à des lettres de prédicat d' arité zéro (qui n'ont pas d'arguments), où ces lettres représentent des propositions , alors ces variables sont des variables propositionnelles , et toute logique de prédicat qui permet d'utiliser des quantificateurs du second ordre pour lier de telles variables propositionnelles est un calcul de prédicat du second ordre, ou logique du second ordre .

Si les variables de prédicat sont également autorisées à être liées à des lettres de prédicat qui sont unaires ou ont une arité supérieure, et lorsque ces lettres représentent des fonctions propositionnelles , telles que le domaine des arguments est mappé sur une gamme de propositions différentes, et lorsque ces variables peuvent être liées par des quantificateurs à de tels ensembles de propositions, alors le résultat est un calcul de prédicat d'ordre supérieur, ou une logique d'ordre supérieur .