Assinatura (lógica)
Na lógica matemática, uma assinatura compreende o conjunto de símbolos não-lógicos que caracteriza uma linguagem formal.
Assinatura em teoria dos modelos editar
Na teoria dos modelos, uma assinatura σ é uma quádrupla (R,F,C,arid), onde:
- R é um conjunto de símbolos de relação ou predicado. Exemplos: ≤, ≥, ∈.
- F é um conjunto de símbolos de funções. Exemplos: +,*.
- C é um conjunto de símbolos para constantes. Exemplos: 0,1.
- arid é a função arid: R ∪ F ∪ C → que indica a aridade dos símbolos de função e relação; as constantes têm por definição aridade 0.
Toda constante pode ser vista como uma função de aridade 0, mas é comum separarmos os símbolos de constantes dos símbolos de funções.
Uma assinatura, mais os símbolos de lógica de primeira ordem, formam uma linguagem de primeira ordem. Os símbolos de funções e constantes da assinatura são usados para formar termos. Esses termos são usados em conjunto com os símbolos de relações para construir fórmulas de primeira ordem. O nome "primeira ordem" se refere ao escopo dos quantificadores: podemos quantificar sobre elementos do universo, mas não sobre subconjuntos ou sobre funções. Por exemplo, muitas sentenças em análise funcional não são sentenças de primeira ordem. Por outro lado, muitas sentenças na teoria elementar dos números são de primeira ordem. Uma sentença é uma fórmula sem variáveis livres. Uma teoria é um conjunto de sentenças, e é dita consistente quando não se chega a uma contradição seguindo-se as regras padrão de inferência. Também é dita fechada se contém todas as consequências de seus elementos; normalmente assume-se que as teorias são consistentes e fechadas.
Exemplo editar
Em um grupo abeliano, temos que R é vazio, F = {+ , -} (-, neste caso, é a função unária que retorna o inverso aditivo de cada elemento) e C = { 0 }. arid então é a função definida por arid(+) = 2, arid(-) = 1 e arid(0) = 0. Uma representação alternativa (mais compacta) é escrever o grupo como e a assinatura como .
Outras convenções em primeira ordem editar
Se não estamos lidando com lógica polissortida, então uma assinatura significa simplesmente
- informar a aridade
- evitar confusão entre símbolos de funções e relações.
Para isso, devemos obedecer dois pré-requisitos:
- particionar o conjunto de símbolos não-lógicos em duas classes: nomes para função e nomes para relação (ou associar um valor binário a cada um desses símbolos, para identificá-los)
- informar a aridade de cada símbolo não-lógico, ou mapeá-los para o conjunto dos números naturais
Há diferentes maneiras de formalizar:
onde F é o conjunto de símbolos não-lógicos para nomes de funções, e R é o conjunto de símbolos não-lógicos para nomes de relações.
Outra maneira:
onde I denota o conjunto de símbolos não-lógicos, e 2 é qualquer conjunto de dois elementos (por exemplo, pode ser uma escolha didática).
Lógica polissortida editar
Em lógica polissortida (em inglês, many-sorted logic, uma tradução da palavra alemã mehrsortig, usada por Arnold Schmidt em um artigo de 1938, cf. Wang 1952)[1], uma assinatura é um conjunto de informações que indica o modo pelo qual os argumentos são preenchidos de forma apropriada: informa a aridade, faz a distinção entre as "partes da fala" que são declarativas ou funcionais. Essa lógica trata de "sorts", que serão chamados aqui de "sortes" - ou "tipo" como nas linguagens de programação que se tem os tipos int, float, double, entre outros.
Borrar ou não editar
Borrar editar
Sortes (contendo uma sorte específica para denotar o tipo de valores verdade) podem ser usadas para "borrar" a distinção entre as partes declarativas e funcionais da fala da linguagem, e entre os símbolos para função (funtores de nome) e símbolos para relação (predicados). Até mesmo conectivos lógicos podem ser tratados dessa forma.
- Conjunto de sortes S
- Conjunto de operações Ω. Cada operação pode ser vista como um nome especial acoplado a um par ordenado: esse par consiste de uma (possivelmente vazia) sequência de sortes, e uma sorte. Isto pode ser formalizado como um mapeamento de um conjunto de nomes de operadores para uma sequência não vazia de sortes.
Não borrar editar
Outro tratamento evita este "embaçamento" (lembrando mais o caso não-sortido)[2]: uma assinatura é um pacote de informação que garante
- distinção entre símbolos de função e símbolos de predicado
- atribui (em ambos os casos) uma sequência de sortes para os símbolos
- no caso de símbolos de funções, uma sequência não vazia (ou um par de uma sequência de sortes possivelmente vazia e de uma sorte)
- no caso de símbolos de relação, uma sequência possivelmente vazia de sortes
Outros aspectos para alternativas editar
Independentemente de borrarmos ou não, constantes podem ser tratadas da mesma forma que símbolos de funções, ou podem ser tratadas como um caso especial (assim como em lógica "não-sortida").
Podemos atribuir para cada variável sua sorte. Mas há uma solução mais dinâmica: variáveis não são tipadas antes de serem usadas em fórmulas ou termos. Fórmulas e termos são necessários para determinar uma tipagem não ambígua para suas variáveis (eles podem não conter nenhuma variável em tipagens diferentes) [3].
Também existem outras (mas, na essência, equivalentes) formalizações. Pode haver também outras variações, como por exemplo, uma variação que permita a sobrecarga de nomes.
Referências
- ↑ Lógica, escrito por Newton C. A. da Costa e Décio Krause.
- ↑ Many-Sorted Logic, o primeiro capítulo em Lecture notes on Decision Procedures, escrito por Calogero G. Zarba.
- ↑ Csirmaz, László: Nemsztenderd analízis. TypoTex Kiadó, Budapest, 1999.
Ver também editar
Bibliografia editar
- Parte do material sobre assinatura em teoria dos modelos retirado de: BEDREGAL, Benjamín R. Callejas; ACIÓLY, Benedito Melo. Lógica para a Ciência da Computação. 2002