Firma (lógica) - Signature (logic)

En lógica , especialmente lógica matemática , una firma enumera y describe los símbolos no lógicos de un lenguaje formal . En álgebra universal , una firma enumera las operaciones que caracterizan una estructura algebraica . En la teoría de modelos , las firmas se utilizan para ambos propósitos. Rara vez se hacen explícitos en tratamientos más filosóficos de la lógica.

Definición

Formalmente, una firma (de un solo orden) se puede definir como una triple σ = ( S func , S rel , ar), donde S func y S rel son conjuntos disjuntos que no contienen ningún otro símbolo lógico básico, llamados respectivamente

  • símbolos de función (ejemplos: +, ×, 0, 1) y
  • símbolos de relación o predicados (ejemplos: ≤, ∈),

y una función ar: S func  S rel → que asigna un número natural llamado aridad a cada función o símbolo de relación. Un símbolo de función o relación se llama n -ary si su aridad es n . Un símbolo de función nulary ( 0 -ary) se llama símbolo constante .  

Una firma sin símbolos de función se llama firma relacional y una firma sin símbolos de relación se llama firma algebraica . Una firma finita es una firma tal que S func y S rel son finitos . De manera más general, la cardinalidad de una firma σ = ( S func , S rel , ar) se define como | σ | = | S func | + | S rel |.

El lenguaje de una firma es el conjunto de todas las oraciones bien formadas construidas a partir de los símbolos de esa firma junto con los símbolos del sistema lógico.

Otras convenciones

En álgebra universal, la palabra tipo o tipo de similitud se utiliza a menudo como sinónimo de "firma". En la teoría de modelos, una firma σ a menudo se denomina vocabulario o se identifica con el lenguaje (de primer orden) L al que proporciona los símbolos no lógicos . Sin embargo, la cardinalidad del lenguaje L siempre será infinita; si σ es finito, entonces | L | será ℵ 0 .

Como la definición formal es inconveniente para el uso diario, la definición de una firma específica a menudo se abrevia de manera informal, como en:

"La firma estándar para los grupos abelianos es σ = (+, -, 0), donde - es un operador unario".

A veces, una firma algebraica se considera simplemente una lista de aridades, como en:

"El tipo de similitud para los grupos abelianos es σ = (2,1,0)".

Formalmente, esto definiría los símbolos de función de la firma como algo así como f 0  (nular), f 1  (unario) y f 2  (binario), pero en realidad los nombres habituales se utilizan incluso en conexión con esta convención.

En lógica matemática , muy a menudo no se permite que los símbolos sean nulos, por lo que los símbolos constantes deben tratarse por separado en lugar de como símbolos de función nula. Forman un conjunto S const disjunto de S func , en el que la función arity ar no está definida. Sin embargo, esto solo sirve para complicar las cosas, especialmente en las pruebas por inducción sobre la estructura de una fórmula, donde se debe considerar un caso adicional. Cualquier símbolo de relación nular, que tampoco está permitido bajo tal definición, puede ser emulado por un símbolo de relación unario junto con una oración que exprese que su valor es el mismo para todos los elementos. Esta traducción falla solo para estructuras vacías (que a menudo están excluidas por convención). Si se permiten símbolos nulares, entonces toda fórmula de lógica proposicional es también una fórmula de lógica de primer orden .

Un ejemplo de una firma infinita usa S func = {+} ∪ {f a : a ∈ F } y S rel = {=} para formalizar expresiones y ecuaciones sobre un espacio vectorial sobre un campo escalar infinito F , donde cada f a denota la operación unaria de multiplicación escalar por a . De esta manera, la firma y la lógica se pueden mantener ordenadas de forma única, siendo los vectores la única clase.

Uso de firmas en lógica y álgebra

En el contexto de la lógica de primer orden , los símbolos de una firma también se conocen como símbolos no lógicos , porque junto con los símbolos lógicos forman el alfabeto subyacente sobre el que se definen inductivamente dos lenguajes formales : El conjunto de términos sobre el firma y el conjunto de fórmulas (bien formadas) sobre la firma.

En una estructura , una interpretación vincula los símbolos de función y relación a objetos matemáticos que justifican sus nombres: La interpretación de un símbolo de función n -aria f en una estructura A con dominio A es una función f A :  A n  →  A , y el La interpretación de un símbolo de relación n -aria es una relación R A  ⊆  A n . Aquí A n = A × A × ... × A denota el producto cartesiano n- veces del dominio A consigo mismo, y entonces f es de hecho una función n -aria y R una relación n -aria.

Firmas de muchos ordenamientos

Para la lógica de muchos tipos y para las estructuras de muchos tipos, las firmas deben codificar información sobre los tipos. La forma más sencilla de hacerlo es a través de tipos de símbolos que desempeñan el papel de aridades generalizadas.

Tipos de símbolo

Sea S un conjunto (de clases) que no contiene los símbolos × o →.

Los tipos de símbolos sobre S son ciertas palabras sobre el alfabeto : los tipos de símbolos relacionales s 1 ×… × s n , y los tipos de símbolos funcionales s 1 ×… × s n → s ′ , para enteros no negativos n y . (Para n = 0, la expresión s 1 ×… × s n denota la palabra vacía).

Firma

Una firma (de muchos ordenamientos) es una triple ( S , P , tipo) que consta de

  • una especie de conjunto S ,
  • un conjunto P de símbolos, y
  • un tipo de mapa que asocia a cada símbolo en P un tipo de símbolo más de S .

Notas

  1. ^ Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (septiembre de 2007). "Búsqueda rápida de cadenas basada en nGram sobre datos codificados mediante firmas algebraicas" (PDF) . 33ª Conferencia Internacional sobre Bases de Datos Muy Grandes (VLDB) . Consultado el 27 de febrero de 2019 . CS1 maint: parámetro desalentado ( enlace )
  2. ^ George Grätzer (1967). "IV. Álgebra Universal". En James C. Abbot (ed.). Tendencias en la teoría de celosía . Princeton / Nueva Jersey: Van Nostrand. págs. 173–210. CS1 maint: parámetro desalentado ( enlace ) Aquí: p.173.
  3. ^ Lógica de muchos ordenamientos , el primer capítulo de las notas de la conferencia sobre procedimientos de decisión , escrito por Calogero G. Zarba .

Referencias

enlaces externos