Assinatura (lógica) - Signature (logic)

Na lógica , especialmente na lógica matemática , uma assinatura lista e descreve os símbolos não lógicos de uma linguagem formal . Na álgebra universal , uma assinatura lista as operações que caracterizam uma estrutura algébrica . Na teoria do modelo , as assinaturas são usadas para ambos os propósitos. Eles raramente são explicitados em tratamentos mais filosóficos da lógica.

Definição

Formalmente, uma assinatura (de classificação única) pode ser definida como um triplo σ = ( S func , S rel , ar), onde S func e S rel são conjuntos disjuntos que não contêm quaisquer outros símbolos lógicos básicos, chamados respectivamente

  • símbolos de função (exemplos: +, ×, 0, 1) e
  • símbolos de relação ou predicados (exemplos: ≤, ∈),

e uma função ar: S func  S rel → que atribui um número natural chamado aridade a cada função ou símbolo de relação. Uma função ou símbolo de relação é denominado n -ary se sua aridade for n . Um símbolo de função nulo ( 0 -ary) é chamado de símbolo de constante .  

Uma assinatura sem símbolos de função é chamada de assinatura relacional e uma assinatura sem símbolos de relação é chamada de assinatura algébrica . Uma assinatura finita é uma assinatura tal que S func e S rel são finitos . De forma mais geral, a cardinalidade de uma assinatura σ = ( S func , S rel , ar) é definida como | σ | = | Função S | + | S rel |.

A linguagem de uma assinatura é o conjunto de todas as sentenças bem formadas construídas a partir dos símbolos dessa assinatura junto com os símbolos do sistema lógico.

Outras convenções

Na álgebra universal, o tipo de palavra ou tipo de semelhança é freqüentemente usado como sinônimo de "assinatura". Na teoria do modelo, uma assinatura σ é freqüentemente chamada de vocabulário ou identificada com a linguagem (de primeira ordem) L para a qual fornece os símbolos não lógicos . No entanto, a cardinalidade da linguagem L sempre será infinita; se σ for finito então | L | será 0 .

Como a definição formal é inconveniente para o uso diário, a definição de uma assinatura específica é muitas vezes abreviada de forma informal, como em:

"A assinatura padrão para grupos abelianos é σ = (+, -, 0), onde - é um operador unário."

Às vezes, uma assinatura algébrica é considerada apenas uma lista de aridades, como em:

"O tipo de similaridade para grupos abelianos é σ = (2,1,0)."

Formalmente, isso definiria os símbolos de função da assinatura como algo como f 0  (nulo), f 1  (unário) ef 2  (binário), mas na realidade os nomes usuais são usados ​​mesmo em conexão com essa convenção.

Na lógica matemática , muitas vezes os símbolos não podem ser nulos, de modo que os símbolos constantes devem ser tratados separadamente, em vez de como símbolos de função nula. Eles formam um conjunto S const disjunto de S func , no qual a função arity ar não é definida. No entanto, isso só serve para complicar as coisas, especialmente em provas por indução sobre a estrutura de uma fórmula, onde um caso adicional deve ser considerado. Qualquer símbolo de relação nula, que também não é permitido por tal definição, pode ser emulado por um símbolo de relação unário junto com uma frase expressando que seu valor é o mesmo para todos os elementos. Esta tradução falha apenas para estruturas vazias (que são frequentemente excluídas por convenção). Se símbolos nulos são permitidos, toda fórmula de lógica proposicional também é uma fórmula de lógica de primeira ordem .

Um exemplo de uma assinatura infinita usa S func = {+} ∪ {f a : a F } e S rel = {=} para formalizar expressões e equações sobre um espaço vetorial sobre um campo escalar infinito F , onde cada f a denota a operação unária de multiplicação escalar por a . Dessa forma, a assinatura e a lógica podem ser mantidas em uma única classificação, sendo os vetores a única classificação.

Uso de assinaturas em lógica e álgebra

No contexto da lógica de primeira ordem , os símbolos em uma assinatura também são conhecidos como símbolos não lógicos , porque junto com os símbolos lógicos eles formam o alfabeto subjacente sobre o qual duas linguagens formais são indutivamente definidas: O conjunto de termos sobre o assinatura e o conjunto de fórmulas (bem formadas) sobre a assinatura.

Em uma estrutura , uma interpretação amarra os símbolos de função e relação a objetos matemáticos que justificam seus nomes: A interpretação de um símbolo de função n -ary f em uma estrutura A com domínio A é uma função f A A n  →  A , e o interpretação de um símbolo de relação n -ary é uma relação R A  ⊆  A n . Aqui, A n = A × A × ... × A denota o produto cartesiano n- dobrado do domínio A consigo mesmo, e então f é de fato uma função n -ária, e R uma relação n -ária.

Assinaturas classificadas

Para lógica de classificação múltipla e para estruturas de classificação múltipla, as assinaturas devem codificar informações sobre as classificações. A maneira mais direta de fazer isso é por meio de tipos de símbolo que desempenham o papel de aridades generalizadas.

Tipos de símbolo

Seja S um conjunto (de tipos) que não contém os símbolos × ou →.

Os tipos de símbolo sobre S são certas palavras sobre o alfabeto : os tipos de símbolo relacional s 1 ×… × s n , e os tipos de símbolo funcional s 1 ×… × s ns ′ , para inteiros não negativos n e . (Para n = 0, a expressão s 1 ×… × s n denota a palavra vazia.)

Assinatura

Uma assinatura (de classificação múltipla) é uma assinatura tripla ( S , P , tipo) que consiste em

  • um conjunto S de tipos,
  • um conjunto P de símbolos, e
  • um tipo de mapa que associa a cada símbolo na P um tipo de símbolo ao longo S .

Notas

  1. ^ Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (setembro de 2007). "Pesquisa rápida de string baseada em nGram sobre dados codificados usando assinaturas algébricas" (PDF) . 33ª Conferência Internacional sobre Bases de Dados Muito Grandes (VLDB) . Página visitada em 27 de fevereiro de 2019 . CS1 maint: parâmetro desencorajado ( link )
  2. ^ George Grätzer (1967). “IV. Álgebra Universal”. Em James C. Abbot (ed.). Trends in Lattice Theory . Princeton / NJ: Van Nostrand. pp. 173–210. CS1 maint: parâmetro desencorajado ( link ) Aqui: p.173.
  3. ^ Many-Sorted Logic , o primeiro capítulo nas notas da aula sobre procedimentos de decisão , escrito por Calogero G. Zarba .

Referências

links externos