L'ensemble des symboles non logiques (prédicats, fonctions et constantes) ainsi que les tris éventuels qui définit la signature d'un langage formel.

Principe

Un vocabulaire (signature) fixe les symboles primitifs, leurs arités et leurs tris ; il détermine quelles formules et quels termes sont bien formés et contraint la classe d'interprétations en spécifiant les symboles auxquels on doit attribuer des significations.

Démonstration

Un vocabulaire Σ peut contenir un prédicat binaire R, une fonction unaire f et des constantes c,d ; le langage construit à partir de Σ permet des termes comme f(f(c)) et des formules comme ∃x R(f(x),d) selon les arités et tris de Σ.

Mauvaise application

Utiliser des symboles hors du vocabulaire déclaré ou changer l'arité d'un symbole au cours d'une démonstration — par exemple traiter R comme binaire à une étape et ternaire à la suivante — viole les règles de formation et invalide les dérivations.

Conséquence

Un vocabulaire clairement spécifié fournit un cadre stable pour la syntaxe, la sémantique et la théorie de la preuve : il assure la bien-formation, l'interprétation uniforme dans les modèles et des énoncés précis sur l'expressibilité et la définissabilité.

Inversion

Si le vocabulaire pouvait varier arbitr airement au sein d'une théorie, la cohérence syntaxique et les comparaisons sémantiques entre modèles s'effondreraient ; les théories n'auraient pas un ensemble stable de symboles primitifs.

Limite

N'inclut pas les symboles logiques (connecteurs, quantificateurs) qui sont généralement fixes, ni la notation métalinguistique ; peut inclure ou non l'égalité ou des déclarations de types/tris selon le formalisme.

Tension sémantique

Tension entre l'usage d'un vocabulaire minimal pour favoriser la généralité et l'extension du vocabulaire pour nommer des concepts commodes ; ajouter des symboles facilite l'expression mais peut obscurcir les relations de définissabilité et d'interprétabilité relative.

Synthèse

Un vocabulaire est la signature du langage : la collection finie ou infinie de symboles de prédicat, de fonction et de constante (et de tris) dont les arités et identités déclarées déterminent la formation des termes et formules et l'interprétation exigée pour les modèles.