En lógica matemática , la lógica monoidal basada en la norma t (o en breve MTL ), la lógica de las t-normas continuas a la izquierda , es una de las lógicas difusas de la t-norma . Pertenece a la clase más amplia de lógicas subestructurales o lógicas de retículas residuales ; [1] extiende la lógica de las celosías residuales integrales acotadas conmutativas (conocidas como lógica monoidal de Höhle , FL ew de Ono , o lógica intuicionista sin contracción) por el axioma de prelinealidad.
Motivación
En lógica difusa , en lugar de considerar los enunciados como verdaderos o falsos, asociamos cada enunciado con una confianza numérica en ese enunciado. Por convención, las confidencias se extienden sobre el intervalo de la unidad, donde la máxima confianza corresponde al concepto clásico de verdadero y al mínimo de confianza corresponde al concepto clásico de falso.
Las normas T son funciones binarias en el intervalo unitario real [0, 1], que en lógica difusa se utilizan a menudo para representar una conjunción conectiva; Si son las confidencias que atribuimos a las declaraciones y respectivamente, entonces se usa una t-norma para calcular la confianza adscrito al enunciado compuesto ' y '. Una t-norma tiene que satisfacer las propiedades de
- conmutatividad,
- asociatividad,
- monotonicidad - si y luego ,
- y tener 1 como elemento de identidad.
Notablemente ausente de esta lista está la propiedad de la idempotencia ; lo más cercano que uno se pone es que. Puede parecer extraño tener menos confianza en ' y 'que en solo , pero en general queremos permitir que la confianza en un combinado ' y ser menos que ambos la confianza en y la confianza en , y luego el pedido por monotonicidad requiere . Otra forma de decirlo es que la t-norma solo puede tomar en cuenta las confidencias como números, no las razones que pueden estar detrás de atribuir esas confidencias; por lo que no puede tratar ' y 'diferente a' y , donde tenemos la misma confianza en ambos '.
Porque el simbolo Debido a que su uso en la teoría de la red está muy estrechamente asociado con la propiedad de idempotencia, puede ser útil cambiar a un símbolo diferente para la conjunción que no sea necesariamente idempotente. En la tradición de la lógica difusa, a veces se usapara esta conjunción "fuerte", pero este artículo sigue la tradición lógica subestructural de usarpor la conjunción fuerte; por lo tanto es la confianza que atribuimos a la declaración (todavía leer ' y ', quizás con' fuerte 'o' multiplicativo 'como calificación de' y ').
Habiendo formalizado la conjunción , se desea continuar con los otros conectivos. Un enfoque para hacer eso es introducir la negación como un mapa de inversión de orden., luego definiendo los conectivos restantes utilizando las leyes de De Morgan , la implicación material y similares. Un problema de hacerlo es que las lógicas resultantes pueden tener propiedades indeseables: pueden estar demasiado cerca de la lógica clásica o, por el contrario, no admitir las reglas de inferencia esperadas . Una alternativa que hace que las consecuencias de diferentes elecciones sean más predecibles es continuar con la implicación. como el segundo conectivo: este es en general el conectivo más común en las axiomatizaciones de la lógica, y tiene vínculos más estrechos con los aspectos deductivos de la lógica que la mayoría de los otros conectivos. Una contraparte de confianzade la implicación conectiva puede, de hecho, definirse directamente como el residuo de la t-norma.
El vínculo lógico entre conjunción e implicación lo proporciona algo tan fundamental como la regla de inferencia modus ponens : de y sigue . En el caso de la lógica difusa que se escribe más rigurosamente como, porque esto hace explícito que nuestra confianza en la (s) premisa (s) aquí es que en , no los de y por separado. Así que si y son nuestras confianzas en y respectivamente, entonces es la confianza buscada en , y es la confianza combinada en . Requerimos que
desde nuestra confianza por no debe ser menor que nuestra confianza en la declaración a partir del cual sigue lógicamente. Esto limita la confianza buscada, y un enfoque para girar en una operación binaria como sería hacerlo lo más grande posible respetando este límite:
- .
Tomando da , por lo que el supremo es siempre de un conjunto acotado no vacío y, por lo tanto, bien definido. Para una norma t general, queda la posibilidad de que tiene una discontinuidad de salto en , en ese caso podría salir estrictamente más grande que aunque se define como el límite superior mínimo de s satisfactorio ; para prevenir eso y tener el trabajo de construcción como se espera, requerimos que la norma tes continuo a la izquierda . El residuo de una t-norma continua a la izquierda, por tanto, puede caracterizarse como la función más débil que hace válido el modus ponens difuso, lo que lo convierte en una función de verdad adecuada para su implicación en lógica difusa.
Más algebraicamente, decimos que una operación es un residuo de una norma t si por todos , , y satisface
- si y solo si .
Esta equivalencia de comparaciones numéricas refleja la equivalencia de implicaciones
- si y solo si
que existe porque cualquier prueba de desde la premisa se puede convertir en una prueba de desde la premisa haciendo un paso adicional de introducción de implicaciones y, a la inversa, cualquier prueba de desde la premisa se puede convertir en una prueba de desde la premisa haciendo un paso adicional de eliminación de implicaciones . La continuidad izquierda de la t-norma es la condición necesaria y suficiente para que se mantenga esta relación entre una conjunción de t-norma y su implicación residual.
Las funciones de verdad de otras conectivas proposicionales se pueden definir por medio de la norma t y su residuo, por ejemplo, la negación residual De esta manera, la t-norma continua a la izquierda, su residuo y las funciones de verdad de conectivos proposicionales adicionales (ver la sección Semántica estándar a continuación) determinan los valores de verdad de fórmulas proposicionales complejas en [0, 1]. Las fórmulas que siempre evalúan a 1 se denominan tautologías con respecto a la norma t continua a la izquierda dada o tautologías. El conjunto de todostautologías se llama la lógica de la t-normaya que estas fórmulas representan las leyes de la lógica difusa (determinadas por la norma t) que se mantienen (hasta el grado 1) independientemente de los grados de verdad de las fórmulas atómicas . Algunas fórmulas son tautologías con respecto a todas las t-normas continuas a la izquierda: representan leyes generales de lógica proposicional difusa que son independientes de la elección de una norma t continua a la izquierda particular. Estas fórmulas forman la lógica MTL, que por lo tanto se puede caracterizar como la lógica de las t-normas continuas a la izquierda. [2]
Sintaxis
Idioma
El lenguaje de la lógica proposicional MTL consiste en numerablemente muchas variables proposicionales y las siguientes primitivas conectores lógicos :
- Implicación ( binario )
- Fuerte conjunción (binario). El signo & es una notación más tradicional para la conjunción fuerte en la literatura sobre lógica difusa, mientras que la notación sigue la tradición de las lógicas subestructurales.
- Conjunción débil (binario), también llamada conjunción reticular (como siempre se realiza mediante la operación reticular de meet en semántica algebraica). A diferencia de BL y las lógicas difusas más fuertes, la conjunción débil no se puede definir en MTL y debe incluirse entre las conectivas primitivas.
- Fondo ( nulary - una constante proposicional ; o son tokens alternativos comunes y cero un nombre alternativo común para la constante proposicional (ya que las constantes bottom y cero de las lógicas subestructurales coinciden en MTL).
Las siguientes son las conectivas lógicas definidas más comunes:
- Negación ( unario ), definido como
- Equivalencia (binario), definido como
- En MTL, la definición es equivalente a
- (Débil) disyunción (binario), también llamada disyunción de celosía (como siempre se realiza mediante la operación de celosía de unión en semántica algebraica), definida como
- Cima (nulary), también llamado uno y denotado por o (ya que las constantes top y cero de las lógicas subestructurales coinciden en MTL), definido como
Las fórmulas bien formadas de MTL se definen como es habitual en las lógicas proposicionales . Para guardar paréntesis, es común usar el siguiente orden de precedencia:
- Conectivos unarios (se unen más estrechamente)
- Conectivos binarios distintos de la implicación y la equivalencia
- Implicación y equivalencia (se unen más libremente)
Axiomas
Un sistema de deducción de estilo de Hilbert para MTL ha sido introducido por Esteva y Godo (2001). Su única regla de derivación es modus ponens :
- de y derivar
Los siguientes son sus esquemas de axiomas :
La numeración tradicional de axiomas, dada en la columna de la izquierda, se deriva de la numeración de axiomas de la lógica difusa básica BL de Hájek . [3] Los axiomas (MTL4a) - (MTL4c) reemplazan el axioma de divisibilidad (BL4) de BL. Los axiomas (MTL5a) y (MTL5b) expresan la ley de residuación y el axioma (MTL6) corresponde a la condición de prelinealidad . Se demostró que los axiomas (MTL2) y (MTL3) del sistema axiomático original eran redundantes (Chvalovský, 2012) y (Cintula, 2005). Todos los demás axiomas demostraron ser independientes (Chvalovský, 2012).
Semántica
Al igual que en otras lógicas difusas de norma t proposicional , la semántica algebraica se usa predominantemente para MTL, con tres clases principales de álgebras con respecto a las cuales la lógica es completa :
- Semántica general , formada por todas las álgebras MTL , es decir, todas las álgebras para las que la lógica es sólida.
- Semántica lineal , formada por todas las álgebras MTL lineales , es decir, todas las álgebras MTL cuyo orden de celosía es lineal.
- Semántica estándar , formada por todas las álgebras MTL estándar , es decir, todas las álgebras MTL cuya red reductora es el intervalo unitario real [0, 1] con el orden habitual; están determinados de forma única por la función que interpreta la conjunción fuerte, que puede ser cualquier norma t continua a la izquierda
Semántica general
MTL-álgebras
Las álgebras para las que la lógica MTL es sólida se denominan MTL-álgebras. Se pueden caracterizar como rejillas residuales integrales acotadas conmutativas prelineales. Más detalladamente, una estructura algebraica es un álgebra MTL si
- es una celosía limitada con el elemento superior 0 y el elemento inferior 1
- es un monoide conmutativo
- y formar un par adjunto , es decir, si y solo si dónde es el orden de celosía de para todo x , y y z en, (la condición de residuo )
- válido para todos los x y y en L (el prelinearity condición)
Ejemplos importantes de álgebras MTL son las álgebras MTL estándar en el intervalo de unidad real [0, 1]. Otros ejemplos incluyen todas las álgebras de Boole , todas las álgebras lineales de Heyting (ambas con), todas las MV-álgebras , todas las BL -álgebras, etc. Dado que la condición de residuación puede expresarse de manera equivalente por identidades, [4] MTL-álgebras forman una variedad .
Interpretación de la lógica MTL en MTL-álgebras
Las conectivas de MTL se interpretan en MTL-álgebras de la siguiente manera:
- Fuerte conjunción por la operación monoidal
- Implicación de la operación (que se llama el residuo de)
- Conjunción débil y disyunción débil por las operaciones de celosía. y respectivamente (generalmente denotado por los mismos símbolos que los conectivos, si no puede surgir confusión)
- Las constantes de verdad cero (arriba) y uno (abajo) por las constantes 0 y 1
- La conectiva de equivalencia es interpretada por la operación definido como
- Debido a la condición de prelinealidad, esta definición es equivalente a una que usa en vez de por lo tanto
- La negación es interpretada por la operación definible
Con esta interpretación de conectivos, cualquier evaluación e v de variables proposicionales en L se extiende únicamente a una evaluación e de todas las fórmulas bien formadas de MTL, mediante la siguiente definición inductiva (que generaliza las condiciones de verdad de Tarski ), para cualquier fórmula A , B , y cualquier variable proposicional p :
De manera informal, el valor de verdad 1 representa la verdad total y el valor de verdad 0 representa la falsedad total; los valores de verdad intermedios representan grados de verdad intermedios. Por lo tanto, una fórmula se considera completamente verdadera bajo una evaluación e si e ( A ) = 1. Se dice que una fórmula A es válida en un MTL-álgebra L si es completamente verdadera en todas las evaluaciones en L , es decir, si e ( a ) = 1 para todas las evaluaciones e en L . Algunas fórmulas (por ejemplo, p → p ) son válidas en cualquier álgebra MTL; estos se denominan tautologías de MTL.
La noción de vinculación global (o: consecuencia global ) se define para MTL de la siguiente manera: un conjunto de fórmulas Γ implica una fórmula A (o: A es una consecuencia global de Γ), en símbolossi para cualquier evaluación e en cualquier MTL-álgebra, siempre que e ( B ) = 1 para todas las fórmulas B en Γ, entonces también e ( A ) = 1. Informalmente, la relación de consecuencia global representa la transmisión de la verdad completa en cualquier MTL- álgebra de valores de verdad.
Teoremas generales de solidez e integridad
La lógica MTL es sólida y completa con respecto a la clase de todas las MTL-álgebras (Esteva & Godo, 2001):
- Una fórmula se puede demostrar en MTL si y solo si es válida en todas las álgebras de MTL.
La noción de MTL-álgebra está de hecho tan definida que MTL-álgebras forman la clase de todas las álgebras para las que la lógica MTL es sólida. Además, el teorema de completitud fuerte se cumple: [5]
- Una fórmula A es una consecuencia global en MTL de un conjunto de fórmulas Γ si y solo si A es derivable de Γ en MTL.
Semántica lineal
Como las álgebras para otras lógicas difusas, [6] MTL-álgebras disfrutan de la siguiente propiedad de descomposición lineal subdirecta :
- Cada álgebra MTL es un producto subdirecto de álgebras MTL ordenadas linealmente.
(Un producto subdirecto es una subálgebra del producto directo tal que todos los mapas de proyección son sobreyectivos . Un álgebra MTL está ordenada linealmente si su orden de red es lineal ).
Como consecuencia de la propiedad de descomposición lineal subdirecta de todas las álgebras MTL, el teorema de completitud con respecto a las álgebras MTL lineales (Esteva y Godo, 2001) se cumple:
- Una fórmula se puede demostrar en MTL si y solo si es válida en todas las álgebras MTL lineales .
- Una fórmula A es derivable en MTL de un conjunto de fórmulas Γ si y solo si A es una consecuencia global en todas las álgebras MTL lineales de Γ.
Semántica estándar
Estándares se denominan álgebras MTL cuya red reductora es el intervalo unitario real [0, 1]. Están determinados de forma única por la función de valor real que interpreta la conjunción fuerte, que puede ser cualquier norma t continua a la izquierda . El álgebra MTL estándar determinada por una norma t continua a la izquierda generalmente se denota por En La implicación está representada por el residuo de conjunción débil y disyunción respectivamente por el mínimo y máximo, y las constantes de verdad cero y uno respectivamente por los números reales 0 y 1.
La lógica MTL está completa con respecto a las álgebras MTL estándar; este hecho se expresa mediante el teorema de completitud estándar (Jenei & Montagna, 2002):
- Una fórmula se puede demostrar en MTL si y solo si es válida en todas las álgebras MTL estándar.
Dado que MTL es completo con respecto a las álgebras de MTL estándar, que están determinadas por normas t continuas a la izquierda, a menudo se hace referencia a MTL como la lógica de las normas t continuas a la izquierda (de manera similar a BL es la lógica de las t-normas continuas ).
Bibliografía
- Hájek P., 1998, Metamatemáticas de la lógica difusa . Dordrecht: Kluwer.
- Esteva F. & Godo L., 2001, "Lógica basada en t-norma monoidal: Hacia una lógica de t-normas continuas de izquierda". Conjuntos y sistemas difusos 124 : 271–288.
- Jenei S. & Montagna F., 2002, "Una prueba de integridad estándar de la lógica monoidal MTL de Esteva y Godo". Studia Logica 70 : 184-192.
- Ono, H., 2003, "Lógicas subestructurales y celosías residuales - una introducción". En FV Hendricks, J. Malinowski (eds.): Trends in Logic: 50 Years of Studia Logica, Trends in Logic 20 : 177–212.
- Cintula P., 2005, "Nota breve: Sobre la redundancia del axioma (A3) en BL y MTL". Computación blanda 9 : 942.
- Cintula P., 2006, "Lógicas débilmente implicativas (difusas) I: Propiedades básicas". Archive for Mathematical Logic 45 : 673–704.
- Chvalovský K., 2012, " Sobre la independencia de los axiomas en BL y MTL ". Conjuntos y sistemas difusos 197 : 123–129, doi : 10.1016 / j.fss.2011.10.018 .
Referencias
- ^ Ono (2003).
- ↑ Conjetura de Esteva y Godo quienes introdujeron la lógica (2001), probada por Jenei y Montagna (2002).
- ^ Hájek (1998), Definición 2.2.4.
- ^ La demostración del Lema 2.3.10 en Hájek (1998) para BL-álgebras también puede adaptarse fácilmente para trabajar con MTL-álgebras.
- ^ Una prueba general de la fuerte completitud con respecto a todas las L -álgebras para cualquier lógica L débilmente implicativa(que incluye MTL) se puede encontrar en Cintula (2006).
- ^ Cintula (2006).