## [Signature](/fr/node/60068) Définition La spécification du vocabulaire non logique d'un langage formel : un ensemble de déclarations de symboles comprenant des symboles constants, des symboles de fonction avec leur arité, et des symboles de relation (prédicats) avec leur arité, qui déterminent les éléments syntaxiques disponibles pour former termes et formules atomiques. ## Principe Principe La signature fixe le vocabulaire et les arités du langage de sorte que les structures interprètent exactement ces symboles ; les notions sémantiques et syntaxiques (structures, homomorphismes, théories, formules) sont définies relativement à une signature donnée et varient lorsque la signature change. ## Démonstration Démonstration Une signature arithmétique typique Σ = {0 : constante, s : fonction unaire, + : fonction binaire, × : fonction binaire} détermine que les termes se construisent à partir de 0 et d'applications de s, +, ×, et que les modèles de Σ doivent fournir des interprétations pour ces symboles sur un certain domaine. ## Mauvaise application Mauvaise application Changer la signature au milieu d'une preuve ou ajouter des symboles tacitement sans enregistrer leurs arités, confondre la signature avec une théorie en traitant des axiomes comme partie de la signature, ou supposer l'équivalence de sens des symboles entre signatures différentes sans traduction. ## Conséquence Conséquence Fixer une signature permet des définitions précises des structures, morphismes et de la satisfaction ; elle contrôle quelles expressions et propriétés sont exprimables et soutient les comparaisons entre modèles et les résultats de transfert (par ex. homomorphismes, plongements, réducts et expansions). ## Inversion Inversion Une théorie est l'inverse en ce qu'elle consiste en axiomes formulés dans un langage sur une signature ; une théorie restreint ou étend la classe de modèles pour une signature donnée mais ne modifie pas les symboles primitifs autorisés sauf en changeant la signature. ## Limite Limite Les signatures concernent uniquement les symboles non logiques et leurs arités ; elles excluent les connecteurs logiques, les quantificateurs et dispositifs méta‑logiques, bien que les signatures à plusieurs sortes, typées ou dotées d'une structure syntaxique supplémentaire soient des généralisations explicites possibles. ## Tension sémantique Tension sémantique Tension entre 'signature' et 'langage' ou 'vocabulaire' dans l'usage informel : la signature est la déclaration formelle des symboles et arités, tandis que 'langage' peut englober les règles de formation syntaxique et les symboles logiques ; une autre tension concerne signatures fixes versus signatures extensibles en spécification modulaire. ## Synthèse Synthèse Une signature est l'énumération formelle des symboles constants, de fonction et de relation avec leurs arités qui définit les expressions primitives admissibles d'un langage formel ; elle établit le cadre pour construire des termes, formuler des formules et interpréter des structures et des morphismes.