Signature (logique) - Signature (logic)

En logique , en particulier en logique mathématique , une signature répertorie et décrit les symboles non logiques d'un langage formel . En algèbre universelle , une signature répertorie les opérations qui caractérisent une structure algébrique . Dans la théorie des modèles , les signatures sont utilisées à ces deux fins. Ils sont rarement rendus explicites dans des traitements plus philosophiques de la logique.

Définition

Formellement, une signature (triée simple) peut être définie comme un triple σ = ( S func , S rel , ar), où S func et S rel sont des ensembles disjoints ne contenant aucun autre symbole logique de base, appelés respectivement

  • symboles de fonction (exemples: +, ×, 0, 1) et
  • symboles de relation ou prédicats (exemples: ≤, ∈),

et une fonction ar: S func  S rel → qui attribue un nombre naturel appelé arité à chaque fonction ou symbole de relation. Un symbole de fonction ou de relation est appelé n -ary si son arité est n . Un symbole de fonction nullaire ( 0 -ary) est appelé un symbole constant .  

Une signature sans symboles de fonction est appelée une signature relationnelle , et une signature sans symboles de relation est appelée une signature algébrique . Une signature finie est une signature telle que S func et S rel sont finies . Plus généralement, la cardinalité d'une signature σ = ( S func , S rel , ar) est définie par | σ | = | S func | + | S rel |.

La langue d'une signature est l'ensemble de toutes les phrases bien formées construites à partir des symboles de cette signature avec les symboles du système logique.

Autres conventions

En algèbre universelle, le mot type ou type de similarité est souvent utilisé comme synonyme de «signature». Dans la théorie des modèles, une signature σ est souvent appelée un vocabulaire , ou identifiée avec le langage (de premier ordre) L auquel elle fournit les symboles non logiques . Cependant, la cardinalité du langage L sera toujours infinie; si σ est fini alors | L | sera 0 .

Comme la définition formelle n'est pas pratique pour un usage quotidien, la définition d'une signature spécifique est souvent abrégée de manière informelle, comme dans:

"La signature standard pour les groupes abéliens est σ = (+, -, 0), où - est un opérateur unaire."

Parfois, une signature algébrique est considérée comme une simple liste d'arités, comme dans:

"Le type de similitude pour les groupes abéliens est σ = (2,1,0)."

Formellement, cela définirait les symboles de fonction de la signature comme quelque chose comme f 0  (nullaire), f 1  (unaire) et f 2  (binaire), mais en réalité les noms usuels sont utilisés même en relation avec cette convention.

En logique mathématique , très souvent, les symboles ne sont pas autorisés à être nuls, de sorte que les symboles constants doivent être traités séparément plutôt que comme des symboles de fonction nulles. Ils forment un ensemble S const disjoint de S func , sur lequel la fonction d'arité ar n'est pas définie. Cependant, cela ne fait que compliquer les choses, en particulier dans les preuves par récurrence sur la structure d'une formule, où un cas supplémentaire doit être considéré. Tout symbole de relation nul, qui n'est pas non plus autorisé dans une telle définition, peut être émulé par un symbole de relation unaire avec une phrase exprimant que sa valeur est la même pour tous les éléments. Cette traduction échoue uniquement pour les structures vides (qui sont souvent exclues par convention). Si les symboles nuls sont autorisés, alors chaque formule de logique propositionnelle est également une formule de logique du premier ordre .

Un exemple de signature infinie utilise S func = {+} ∪ {f a : a F } et S rel = {=} pour formaliser des expressions et des équations sur un espace vectoriel sur un champ scalaire infini F , où chaque f a désigne l'opération unaire de multiplication scalaire par a . De cette façon, la signature et la logique peuvent être conservées en tri simple, les vecteurs étant le seul tri.

Utilisation des signatures en logique et en algèbre

Dans le contexte de la logique du premier ordre , les symboles d'une signature sont également connus sous le nom de symboles non logiques , car avec les symboles logiques, ils forment l'alphabet sous-jacent sur lequel deux langages formels sont définis de manière inductive: L'ensemble des termes sur le signature et l'ensemble des formules (bien formées) sur la signature.

Dans une structure , une interprétation lie les symboles de fonction et de relation à des objets mathématiques qui justifient leurs noms: L'interprétation d'un symbole de fonction n -ary f dans une structure A de domaine A est une fonction f A A n  →  A , et le l'interprétation d'un symbole de relation n -ary est une relation R A  ⊆  A n . Ici A n = A × A × ... × A désigne le produit cartésien n- fois du domaine A avec lui-même, et donc f est en fait une fonction n -ary, et R une relation n -ary.

Signatures triées de manière multiple

Pour la logique à tri multiple et pour les structures à tri multiple, les signatures doivent encoder des informations sur les tris. Le moyen le plus simple de le faire est d' utiliser des types de symboles qui jouent le rôle d'arités généralisées.

Types de symboles

Soit S un ensemble (de sortes) ne contenant pas les symboles × ou →.

Les types de symboles sur S sont certains mots sur l'alphabet : les types de symboles relationnels s 1 ×… × s n , et les types de symboles fonctionnels s 1 ×… × s ns ′ , pour les entiers non négatifs n et . (Pour n = 0, l'expression s 1 ×… × s n désigne le mot vide.)

Signature

Une signature (triée en plusieurs) est un triple (type S , P ) constitué de

  • un ensemble S de sortes,
  • un ensemble P de symboles, et
  • un type de carte qui associe à chaque symbole dans P un type de symbole sur S .

Remarques

  1. ^ Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (septembre 2007). «Recherche rapide de chaîne basée sur nGram sur les données encodées à l'aide de signatures algébriques» (PDF) . 33e Conférence internationale sur les très grandes bases de données (VLDB) . Récupéré le 27 février 2019 . CS1 maint: paramètre découragé ( lien )
  2. ^ George Grätzer (1967). "IV. Algèbre Universelle". Dans James C. Abbot (éd.). Tendances de la théorie des treillis . Princeton / NJ: Van Nostrand. 173-210. CS1 maint: paramètre découragé ( lien ) Ici: p.173.
  3. ^ Many-Sorted Logic , le premier chapitre des notes de cours sur les procédures de décision , écrit par Calogero G. Zarba .

Les références

Liens externes