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 n → s ′ , 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
- ^ 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 )
- ^ 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.
- ^ Many-Sorted Logic , o primeiro capítulo nas notas da aula sobre procedimentos de decisão , escrito por Calogero G. Zarba .
Referências
- Burris, Stanley N .; Sankappanavar, HP (1981). Um Curso de Álgebra Universal . Springer . ISBN 3-540-90578-2 . Edição online gratuita .
- Hodges, Wilfrid (1997). A Shorter Model Theory . Cambridge University Press . ISBN 0-521-58713-1 .
links externos
- Stanford Encyclopedia of Philosophy : " Model theory " - por Wilfred Hodges .
- PlanetMath: A entrada " Assinatura " descreve o conceito para o caso em que nenhuma classificação é introduzida.
- Baillie, Jean , " Uma introdução à especificação algébrica de tipos de dados abstratos. "