En lógica , una regla de inferencia es admisible en un sistema formal si el conjunto de teoremas del sistema no cambia cuando esa regla se agrega a las reglas existentes del sistema. En otras palabras, cada fórmula que se puede derivar usando esa regla ya es derivable sin esa regla, por lo que, en cierto sentido, es redundante. Paul Lorenzen (1955) introdujo el concepto de regla admisible .
Definiciones
La admisibilidad se ha estudiado sistemáticamente sólo en el caso de reglas estructurales en lógicas proposicionales no clásicas , que describiremos a continuación.
Sea fijo un conjunto de conectivos proposicionales básicos (por ejemplo,en el caso de las lógicas superintuicionistas , oen el caso de las lógicas monomodales ). Las fórmulas bien formadas se construyen libremente usando estas conectivas a partir de un conjunto numerable infinito de variables proposicionales p 0 , p 1 , .... Una sustitución σ es una función de fórmulas a fórmulas que conmuta con las conectivas, es decir,
para cada conectivo f , y fórmulas A 1 , ..., A n . (También podemos aplicar sustituciones a conjuntos Γ de fórmulas, haciendo σΓ = {σ A : A ∈ Γ}. ) Una relación de consecuencia al estilo de Tarski [1] es una relación entre conjuntos de fórmulas y fórmulas, de modo que
- Si luego
- Si y luego
para todas las fórmulas A , B y conjuntos de fórmulas Γ, Δ. Una relación de consecuencia tal que
- Si luego
para todas las sustituciones σ se llama estructural . (Nótese que el término "estructural", tal como se utiliza aquí y a continuación, no está relacionado con la noción de reglas estructurales en los cálculos posteriores .) Una relación de consecuencia estructural se denomina lógica proposicional . Una fórmula A es un teorema de una lógica Si .
Por ejemplo, identificamos una lógica superintuicionista L con su relación de consecuencia estándaraxiomatizable por modus ponens y axiomas, e identificamos una lógica modal normal con su relación de consecuencia global axiomatizado por modus ponens, necessitation y axiomas.
Una regla de inferencia estructural [2] (o simplemente una regla para abreviar) viene dada por un par (Γ, B ), generalmente escrito como
donde Γ = { A 1 , ..., A n } es un conjunto finito de fórmulas y B es una fórmula. Una instancia de la regla es
para una sustitución σ. La regla Γ / B es derivable en, Si . Es admisible si para cada instancia de la regla, σ B es un teorema siempre que todas las fórmulas de σΓ sean teoremas. [3] En otras palabras, una regla es admisible si, cuando se agrega a la lógica, no conduce a nuevos teoremas. [4] También escribimossi Γ / B es admisible. (Tenga en cuenta que es una relación de consecuencia estructural en sí misma.)
Todas las reglas derivables son admisibles, pero no al revés en general. Una lógica es estructuralmente completa si toda regla admisible es derivable, es decir,. [5]
En lógicas con una conjunción conectiva de buen comportamiento (como las lógicas superintuicionista o modal), una regla es equivalente a con respecto a la admisibilidad y derivabilidad. Por tanto, es habitual tratar sólo con unarios reglas A / B .
Ejemplos de
- El cálculo proposicional clásico ( CPC ) está estructuralmente completo. [6] De hecho, suponga que A / B es una regla no derivable y fije una asignación v tal que v ( A ) = 1 yv ( B ) = 0. Defina una sustitución σ tal que para cada variable p , σ p =si v ( p ) = 1, y σ p =si v ( p ) = 0. Entonces σ A es un teorema, pero σ B no lo es (de hecho, ¬σ B es un teorema). Por tanto, la regla A / B tampoco es admisible. (El mismo argumento se aplica a cualquier L lógica multivalor completa con respecto a una matriz lógica cuyos elementos tienen un nombre en el lenguaje de L. )
- La regla de Kreisel - Putnam (también conocida como regla de Harrop , o regla de independencia de la premisa)
- es admisible en el cálculo proposicional intuicionista ( IPC ). De hecho, es admisible en toda lógica superintuicionista. [7] Por otro lado, la fórmula
- no es una tautología intuicionista, por lo tanto, KPR no se puede derivar en IPC . En particular, IPC no es estructuralmente completo.
- La regla
- es admisible en muchas lógicas modales, como K , D , K 4, S 4, GL (consulte esta tabla para ver los nombres de las lógicas modales). Es derivable en S 4, pero no derivable en K , D , K 4 o GL .
- La regla
- es admisible en toda lógica modal normal. [8] Es derivable en GL y S 4.1, pero no es derivable en K , D , K 4, S 4, S 5.
- es admisible (pero no derivable) en la lógica modal básica K , y es derivable en GL . Sin embargo, LR no es admisible en K 4. En particular, es no cierto en general que un admisible regla en una lógica L debe ser admisible en sus extensiones.
- La lógica de Gödel-Dummett ( LC ) y la lógica modal Grz .3 son estructuralmente completas. [9] La lógica difusa del producto también es estructuralmente completa. [10]
Decidibilidad y reglas reducidas
La pregunta básica sobre las reglas admisibles de una lógica dada es si el conjunto de todas las reglas admisibles es decidible . Tenga en cuenta que el problema no es trivial incluso si la lógica en sí (es decir, su conjunto de teoremas) es decidible : la definición de admisibilidad de una regla A / B implica un cuantificador universal ilimitado sobre todas las sustituciones proposicionales, por lo tanto, a priori , solo sabemos que la admisibilidad de regla en una lógica decidible es(es decir, su complemento es recursivamente enumerable ). Por ejemplo, se sabe que la admisibilidad en las lógicas bimodales K u y K 4 u (las extensiones de K o K 4 con la modalidad universal ) es indecidible. [11] Sorprendentemente, la decidibilidad de la admisibilidad en la lógica modal básica K es un gran problema abierto.
No obstante, se sabe que la admisibilidad de las reglas es decidible en muchas lógicas modales y superintuicionistas. Los primeros procedimientos de decisión para reglas admisibles en lógicas modales transitivas básicas fueron construidos por Rybakov , utilizando la forma reducida de reglas . [12] Una regla modal en las variables p 0 , ..., p k se llama reducida si tiene la forma
donde cada está en blanco o es negación . Para cada regla r , podemos construir efectivamente una regla reducida s (llamada la forma reducida de r ) tal que cualquier lógica admita (o derive) r si y solo si admite (o deriva) s , mediante la introducción de variables de extensión para todas las subfórmulas en A , y expresando el resultado en la forma normal disyuntiva completa . Por lo tanto, es suficiente construir un algoritmo de decisión para la admisibilidad de reglas reducidas.
Dejar ser una regla reducida como arriba. Identificamos cada conjunción con el set de sus coyunturas. Para cualquier subconjunto W del conjuntode todas las conjunciones, definamos un modelo de Kripke por
Entonces, lo siguiente proporciona un criterio algorítmico para la admisibilidad en K 4: [13]
Teorema . La reglano es admisible en K 4 si y solo si existe un conjunto tal que
- para algunos
- para cada
- para cada subconjunto D de W existen elementos tal que las equivalencias
- si y solo si para cada
- si y solo si y para cada
- mantener para todos j .
Se pueden encontrar criterios similares para las lógicas S 4, GL y Grz . [14] Además, la admisibilidad en lógica intuicionista puede reducirse a admisibilidad en Grz utilizando la traducción de Gödel-McKinsey-Tarski : [15]
- si y solo si
Rybakov (1997) desarrolló técnicas mucho más sofisticadas para mostrar la decidibilidad de la admisibilidad, que se aplican a una clase robusta (infinita) de lógica transitiva (es decir, ampliando K 4 o IPC ) modal y superintuicionista, incluyendo p. Ej. S 4.1, S 4.2, S 4.3 , KC , T k (así como las lógicas mencionadas anteriormente IPC , K 4, S 4, GL , Grz ). [dieciséis]
A pesar de ser decidible, el problema de admisibilidad tiene una complejidad computacional relativamente alta , incluso en lógicas simples: la admisibilidad de reglas en las lógicas transitivas básicas IPC , K 4, S 4, GL , Grz es coNEXP -completa. [17] Esto debería contrastarse con el problema de derivabilidad (para reglas o fórmulas) en estas lógicas, que es PSPACE -completo. [18]
Proyectividad y unificación
La admisibilidad en la lógica proposicional está estrechamente relacionada con la unificación en la teoría ecuacional de las álgebras modales o de Heyting . La conexión fue desarrollada por Ghilardi (1999, 2000). En la configuración lógica, un unificador de una fórmula A en una lógica L (una L -unifier para abreviar) es una sustitución σ tal que σ A es un teorema de L . (Usando esta noción, podemos reformular la admisibilidad de una regla A / B en L como "cada L -unificador de A es un L -unificador de B ".) Un L -unificador σ es menos general que un L -unificador τ, escrito como σ ≤ τ, si existe una sustitución υ tal que
para cada variable p . Un conjunto completo de unificadores de una fórmula A es un conjunto S de L -unifiers de A tales que cada L -unifier de A es menos general que algunos unificador de S . A unificador general, la mayoría (MGU) de A es un unificador σ tal que {σ} es un conjunto completo de unificadores de A . Se deduce que si S es un conjunto completo de unificadores de A , entonces una regla A / B es L -admissible si y sólo si cada σ en S es un L -unifier de B . Por tanto, podemos caracterizar las reglas admisibles si podemos encontrar conjuntos completos de unificadores que se comporten bien.
Una clase importante de fórmulas que tienen un unificador más general son las fórmulas proyectivas : estas son fórmulas A tales que existe un unificador σ de A tal que
para cada fórmula B . Tenga en cuenta que σ es un MGU de A . En lógicas transitivas modales y superintuicionistas con la propiedad del modelo finito (fmp), se pueden caracterizar semánticamente fórmulas proyectivas como aquellas cuyo conjunto de modelos L finitos tiene la propiedad de extensión : [19] si M es un modelo L finito de Kripke con una raíz r cuyo grupo es un singleton , y la fórmula A se cumple en todos los puntos de M excepto para r , entonces podemos cambiar la valoración de las variables en r para que A sea verdadera también en r . Además, la demostración proporciona una construcción explícita de un mgu para una fórmula proyectiva A dada .
En las lógicas transitivas básicas IPC , K 4, S 4, GL , Grz (y más generalmente en cualquier lógica transitiva con el fmp cuyo conjunto de marco finito satisface otro tipo de propiedad de extensión), podemos construir efectivamente para cualquier fórmula A su proyectiva aproximación Π ( A ): [20] un conjunto finito de fórmulas proyectivas tales que
- para cada
- todo unificador de A es un unificador de una fórmula de Π ( A ).
De ello se deduce que el conjunto de GMSI de elementos de Π ( A ) es un conjunto completo de unificadores de A . Además, si P es una fórmula proyectiva, entonces
- si y solo si
para cualquier fórmula B . Así obtenemos la siguiente caracterización efectiva de las reglas admisibles: [21]
- si y solo si
Bases de reglas admisibles
Sea L una lógica. Un conjunto R de L - regla admisible se denomina base [22] de reglas admisibles, si cada regla admisible Γ / B puede derivarse de R y las reglas derivables de L , usando sustitución, composición y debilitamiento. En otras palabras, R es una base si y solo si es la relación de consecuencia estructural más pequeña que incluye y R .
Nótese que la decidibilidad de las reglas admisibles de una lógica decidible es equivalente a la existencia de bases recursivas (o recursivamente enumerables ): por un lado, el conjunto de todas las reglas admisibles es una base recursiva si la admisibilidad es decidible. Por otro lado, el conjunto de reglas admisibles es siempre básico, y si además tenemos una base re, también lo es, por lo tanto, es decidible. (En otras palabras, podemos decidir la admisibilidad de A / B mediante el siguiente algoritmo : comenzamos en paralelo dos búsquedas exhaustivas , una para una sustitución σ que unifica A pero no B , y otra para una derivación de A / B de R y. Una de las búsquedas tiene que finalmente dar una respuesta.) Aparte de la decidibilidad, las bases explícitas de las reglas admisibles son útiles para algunas aplicaciones, por ejemplo, en la complejidad de la prueba . [23]
Para una lógica dada, podemos preguntarnos si tiene una base recursiva o finita de reglas admisibles y proporcionar una base explícita. Si una lógica no tiene una base finita, no obstante puede tener una base independiente : una base R tal que ningún subconjunto propio de R sea una base.
En general, se puede decir muy poco sobre la existencia de bases con propiedades deseables. Por ejemplo, mientras que las lógicas tabulares generalmente se comportan bien y siempre son finitamente axiomatizables, existen lógicas tabulares modales sin una base de reglas finita o independiente. [24] Las bases finitas son relativamente raras: incluso las lógicas transitivas básicas IPC , K 4, S 4, GL , Grz no tienen una base finita de reglas admisibles, [25] aunque tienen bases independientes. [26]
Ejemplos de bases
- El conjunto vacío es una base de las reglas L -admisibles si y solo si L es estructuralmente completo.
- Cada extensión de la lógica modal S 4.3 (incluyendo, en particular, S 5) tiene una base finita que consiste en la regla única [27]
- Reglas de Visser
- son una base de reglas admisibles en IPC o KC . [28]
- Las normas
- son una base de las reglas admisibles de GL . [29] (Tenga en cuenta que la disyunción vacía se define como .)
- Las normas
- son una base de las reglas admisibles de S 4 o Grz . [30]
Semántica de reglas admisibles
Una regla Γ / B es válida en un marco de Kripke modal o intuicionista , si lo siguiente es cierto para cada valoración en F :
- Si para todos , luego .
(La definición se generaliza fácilmente a marcos generales , si es necesario).
Deje que X sea un subconjunto de W , y t un punto en W . Decimos que t es
- un predecesor reflexivo ajustado de X , si para cada y en W : t R y si y solo si t = y o x = y o x R y para alguna x en X ,
- un apretado predecesor irreflexive de X si para cada y en W : t R y si y sólo si x = y o x R y para algunos x en X .
Podemos decir que una trama F tiene reflexivos (irreflexivas) predecesores apretados, si para cada finita subconjunto X de W , existe una reflexiva (irreflexive) apretada precursor de X en W .
Tenemos: [31]
- una regla es admisible en IPC si y solo si es válida en todos los marcos intuicionistas que tienen predecesores reflexivos ajustados,
- una regla es admisible en K 4 si y solo si es válida en todos los marcos transitivos que tienen predecesores ajustados reflexivos e irreflexivos,
- una regla es admisible en S 4 si y solo si es válida en todos los marcos reflexivos transitivos que tienen predecesores reflexivos ajustados,
- una regla es admisible en GL si y solo si es válida en todos los marcos transitivos inversos bien fundamentados que tienen predecesores irreflexivos ajustados.
Tenga en cuenta que, aparte de unos pocos casos triviales, los marcos con predecesores ajustados deben ser infinitos, por lo tanto, las reglas admisibles en lógicas transitivas básicas no disfrutan de la propiedad del modelo finito.
Completitud estructural
Si bien una clasificación general de lógicas estructuralmente completas no es una tarea fácil, tenemos un buen conocimiento de algunos casos especiales.
La lógica intuicionista en sí misma no es estructuralmente completa, pero sus fragmentos pueden comportarse de manera diferente. Es decir, cualquier regla libre de disyunción o regla libre de implicaciones admisible en una lógica superintuicionista es derivable. [32] Por otro lado, la regla de las Mentas
es admisible en la lógica intuicionista pero no derivable, y contiene sólo implicaciones y disyunciones.
Conocemos las lógicas transitivas máximas estructuralmente incompletas. Una lógica se llama estructuralmente completa hereditariamente , si alguna extensión es estructuralmente completa. Por ejemplo, la lógica clásica, así como las lógicas LC y Grz .3 mencionadas anteriormente, son hereditariamente estructuralmente completas. Citkin y Rybakov dieron una descripción completa de lógicas modales transitiva y superintuicionista estructuralmente completas, respectivamente. Es decir, una lógica superintuicionista es estructuralmente completa hereditariamente si y solo si no es válida en cualquiera de los cinco marcos de Kripke [9]
De manera similar, una extensión de K 4 es hereditariamente estructuralmente completa si y solo si no es válida en alguno de los veinte marcos de Kripke (incluidos los cinco marcos intuicionistas anteriores). [9]
Existen lógicas estructuralmente completas que no son estructuralmente completas hereditariamente: por ejemplo, la lógica de Medvedev es estructuralmente completa, [33] pero está incluida en la lógica estructuralmente incompleta KC .
Variantes
Una regla con parámetros es una regla de la forma
cuyas variables se dividen en las variables "regulares" p i , y los parámetros s i . La regla es L -admissible si cada L -unifier σ de A tales que σ s i = s i para cada i es también un unificador de B . Los resultados básicos de decidibilidad para reglas admisibles también se aplican a reglas con parámetros. [34]
Una regla de conclusión múltiple es un par (Γ, Δ) de dos conjuntos finitos de fórmulas, escrito como
Tal regla es admisible si todo unificador de Γ es también un unificador de alguna fórmula de Δ. [35] Por ejemplo, una L lógica es consistente si admite la regla
y una lógica superintuicionista tiene la propiedad de disyunción si admite la regla
Nuevamente, los resultados básicos de las reglas admisibles se generalizan sin problemas a reglas de conclusión múltiple. [36] En lógicas con una variante de la propiedad de disyunción, las reglas de conclusión múltiple tienen el mismo poder expresivo que las reglas de conclusión única: por ejemplo, en S 4 la regla anterior es equivalente a
No obstante, a menudo se pueden emplear reglas de conclusión múltiple para simplificar los argumentos.
En la teoría de la prueba , la admisibilidad se considera a menudo en el contexto de cálculos secuenciales , donde los objetos básicos son secuencias en lugar de fórmulas. Por ejemplo, se puede reformular el teorema de eliminación de cortes diciendo que el cálculo secuencial sin cortes admite la regla de corte
(Por abuso del lenguaje, también se dice a veces que el cálculo secuencial (completo) admite corte, lo que significa que su versión sin cortes lo hace). Sin embargo, la admisibilidad en los cálculos secuenciales suele ser solo una variante de notación para la admisibilidad en la lógica correspondiente: cualquier El cálculo completo para (digamos) lógica intuicionista admite una regla secuencial si y solo si el IPC admite la regla de la fórmula que obtenemos al traducir cada secuencia a su fórmula característica .
Notas
- ^ Blok y Pigozzi (1989), Kracht (2007)
- ↑ Rybakov (1997), Def. 1.1.3
- ↑ Rybakov (1997), Def. 1.7.2
- ^ Del teorema de de Jongh a la lógica intuicionista de las demostraciones
- ↑ Rybakov (1997), Def. 1.7.7
- ^ Chagrov y Zakharyaschev (1997), Thm. 1,25
- ↑ Prucnal (1979), cf. Iemhoff (2006)
- ^ Rybakov (1997), p. 439
- ↑ a b c Rybakov (1997), Thms. 5.4.4, 5.4.8
- ^ Cintula y Metcalfe (2009)
- ^ Wolter y Zakharyaschev (2008)
- ↑ Rybakov (1997), §3.9
- ↑ Rybakov (1997), Thm. 3.9.3
- ^ Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf. Chagrov y Zakharyaschev (1997), §16.7
- ↑ Rybakov (1997), Thm. 3.2.2
- ↑ Rybakov (1997), §3.5
- ↑ Jeřábek (2007)
- ^ Chagrov y Zakharyaschev (1997), §18.5
- ↑ Ghilardi (2000), Thm. 2.2
- ↑ Ghilardi (2000), p. 196
- ↑ Ghilardi (2000), Thm. 3.6
- ↑ Rybakov (1997), Def. 1.4.13
- ^ Mentas y Kojevnikov (2004)
- ↑ Rybakov (1997), Thm. 4.5.5
- ↑ Rybakov (1997), §4.2
- ↑ Jeřábek (2008)
- ↑ Rybakov (1997), Cor. 4.3.20
- ↑ Iemhoff (2001, 2005), Rozière (1992)
- ↑ Jeřábek (2005)
- ↑ Jeřábek (2005 , 2008)
- ^ Iemhoff (2001), Jeřábek (2005)
- ^ Rybakov (1997), Thms. 5.5.6, 5.5.9
- ^ Prucnal (1976)
- ↑ Rybakov (1997), §6.1
- ^ Jeřábek (2005); cf. Kracht (2007), párrafo 7
- ↑ Jeřábek (2005, 2007, 2008)
Referencias
- W. Blok, D. Pigozzi, Lógicas algebraizables , Memorias de la American Mathematical Society 77 (1989), no. 396, 1989.
- A. Chagrov y M. Zakharyaschev, Modal Logic , Oxford Logic Guides vol. 35, Oxford University Press, 1997. ISBN 0-19-853779-4
- P. Cintula y G. Metcalfe, Completitud estructural en lógicas difusas , Notre Dame Journal of Formal Logic 50 (2009), no. 2, págs. 153-182. doi : 10.1215 / 00294527-2009-004
- AI Citkin, Sobre lógicas superintuicionistas estructuralmente completas , Matemáticas soviéticas - Doklady, vol. 19 (1978), págs. 816–819.
- S. Ghilardi, Unificación en lógica intuicionista , Journal of Symbolic Logic 64 (1999), no. 2, págs. 859–880. Proyecto Euclid JSTOR
- S. Ghilardi, Mejor resolución de ecuaciones modales , Annals of Pure and Applied Logic 102 (2000), no. 3, págs. 183–198. doi : 10.1016 / S0168-0072 (99) 00032-9
- R. Iemhoff, Sobre las reglas admisibles de la lógica proposicional intuicionista , Journal of Symbolic Logic 66 (2001), no. 1, págs. 281-294. Proyecto Euclid JSTOR
- R. Iemhoff, Lógica intermedia y reglas de Visser , Notre Dame Journal of Formal Logic 46 (2005), no. 1, págs. 65–81. doi : 10.1305 / ndjfl / 1107220674
- R. Iemhoff, Sobre las reglas de la lógica intermedia , Archive for Mathematical Logic, 45 (2006), no. 5, págs. 581–599. doi : 10.1007 / s00153-006-0320-8
- E. Jeřábek, Reglas admisibles de la lógica modal , Journal of Logic and Computation 15 (2005), no. 4, págs. 411–431. doi : 10.1093 / logcom / exi029
- E. Jeřábek, Complejidad de las reglas admisibles , Archive for Mathematical Logic 46 (2007), no. 2, págs. 73–92. doi : 10.1007 / s00153-006-0028-9
- E. Jeřábek, Bases independientes de reglas admisibles , Logic Journal of the IGPL 16 (2008), no. 3, págs. 249-267. doi : 10.1093 / jigpal / jzn004
- M. Kracht, Relaciones de consecuencia modal , en: Manual de lógica modal (P. Blackburn, J. van Benthem y F. Wolter, eds.), Estudios de lógica y razonamiento práctico, vol. 3, Elsevier, 2007, págs. 492–545. ISBN 978-0-444-51690-9
- P. Lorenzen, Einführung in die operativo Logik und Mathematik , Grundlehren der mathischen Wissenschaften vol. 78, Springer-Verlag, 1955.
- G. Mints y A. Kojevnikov, Los sistemas intuicionistas de Frege son polinomialmente equivalentes , Zapiski Nauchnyh Seminarov POMI 316 (2004), págs. 129-146. PS comprimido con gzip
- T. Prucnal, Completitud estructural del cálculo proposicional de Medvedev , Reports on Mathematical Logic 6 (1976), págs. 103-105.
- T. Prucnal, Sobre dos problemas de Harvey Friedman , Studia Logica 38 (1979), no. 3, págs. 247-262. doi : 10.1007 / BF00405383
- P. Rozière, Règles admissibles en calcul propositionnel intuitionniste , Ph.D. tesis, Université de Paris VII, 1992. PDF
- VV Rybakov, Admisibilidad de las reglas de inferencia lógica , Estudios de lógica y fundamentos de las matemáticas vol. 136, Elsevier, 1997. ISBN 0-444-89505-1
- F. Wolter, M. Zakharyaschev, Indecidibilidad de los problemas de unificación y admisibilidad para lógicas modales y descriptivas , ACM Transactions on Computational Logic 9 (2008), no. 4, artículo no. 25. doi : 10.1145 / 1380572.1380574 PDF