Regla admisible

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 añade a las reglas existentes del sistema. En otras palabras, toda fórmula que se pueda derivar utilizando esa regla ya es derivable sin ella, por lo que, en cierto sentido, es redundante. El concepto de regla admisible fue introducido por Paul Lorenzen (1955).

Definiciones

La admisibilidad ha sido estudiada sistemáticamente sólo en el caso de reglas estructurales (es decir, cerradas a la sustitución ) 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 lógicas superintuicionistas o en el caso de lógicas monomodales ). Se construyen fórmulas bien formadas libremente usando estos conectivos a partir de un conjunto infinito numerable de variables proposicionales p ₀ , p ₁ , .... Una sustitución σ es una función de fórmulas a fórmulas que conmuta con aplicaciones de los conectivos, es decir, ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$ ${\displaystyle \{\to ,\bot ,\Box \}}$

${\displaystyle \sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})}$

para cada conectivo f , y fórmulas A ₁ , ... , A _n . (También podemos aplicar sustituciones a conjuntos Γ de fórmulas, haciendo σ Γ = { σA : A ∈ Γ}. ) Una relación de consecuencia de estilo Tarski ^[1] es una relación entre conjuntos de fórmulas, y fórmulas, tales que ${\displaystyle \vdash }$

1. ${\displaystyle A\vdash A,}$
2. si entonces ("debilitamiento") ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \Gamma ,\Delta \vdash A,}$
3. si y entonces ("composición") ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \Delta ,A\vdash B}$ ${\displaystyle \Gamma ,\Delta \vdash B,}$

para todas las fórmulas A , B y conjuntos de fórmulas Γ, Δ. Una relación de consecuencia tal que

4. Si entonces ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \sigma \Gamma \vdash \sigma A}$

Para todas las sustituciones, σ se denomina estructural . (Tenga en cuenta 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 consecuentes ). Una relación de consecuencia estructural se denomina lógica proposicional . Una fórmula A es un teorema de una lógica si . ${\displaystyle \vdash }$ ${\displaystyle \varnothing \vdash A}$

Por ejemplo, identificamos una lógica superintuicionista L con su relación de consecuencia estándar generada por modus ponens y axiomas, e identificamos una lógica modal normal con su relación de consecuencia global generada por modus ponens, necesidad y (como axiomas) los teoremas de la lógica. ${\displaystyle \vdash _{L}}$ ${\displaystyle \vdash _{L}}$

Una regla de inferencia estructural ^[2] (o simplemente regla para abreviar) está dada por un par (Γ, B ), generalmente escrito como

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,}$

donde Γ = { A ₁ , ... , A _n } es un conjunto finito de fórmulas y B es una fórmula. Una instancia de la regla es

${\displaystyle \sigma A_{1},\dots ,\sigma A_{n}/\sigma B}$

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 escribimos si Γ/ B es admisible. (Obsérvese que es una relación de consecuencia estructural por sí misma). ${\displaystyle \vdash }$ ${\displaystyle \Gamma \vdash B}$ ${\displaystyle \Gamma \mathrel {|\!\!\!\sim } B}$ ${\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}$

Toda regla derivable es admisible, pero no viceversa en general. Una lógica es estructuralmente completa si toda regla admisible es derivable, es decir, . ^[5] ${\displaystyle {\vdash }={\,|\!\!\!\sim }}$

En lógicas con un conectivo de conjunción bien comportado (como las lógicas superintuicionistas o modales), una regla es equivalente a con respecto a la admisibilidad y derivabilidad. Por lo tanto, es habitual tratar solo con reglas unarias A / B . ${\displaystyle A_{1},\dots ,A_{n}/B}$ ${\displaystyle A_{1}\land \dots \land A_{n}/B}$

Ejemplos

• El cálculo proposicional clásico ( CPC ) es estructuralmente completo. ^[6] De hecho, supongamos que A / B es una regla no derivable, y fijemos una asignación v tal que v ( A ) = 1, y v ( B ) = 0. Definamos 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 lo tanto, la regla A / B tampoco es admisible. (El mismo argumento se aplica a cualquier lógica multivaluada L completa con respecto a una matriz lógica cuyos elementos tienen todos un nombre en el lenguaje de L ). ${\displaystyle \top }$ ${\displaystyle \bot }$
• La regla de Kreisel - Putnam (también conocida como regla de Harrop o regla de independencia de las premisas )

${\displaystyle ({\mathit {KPR}})\qquad {\frac {\neg p\to q\lor r}{(\neg p\to q)\lor (\neg p\to r)}}}$

es admisible en el cálculo proposicional intuicionista ( CPI ). De hecho, es admisible en toda lógica superintuicionista. ^[7] Por otra parte, la fórmula

${\displaystyle (\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))}$

no es un teorema intuicionista; por lo tanto, KPR no es derivable en IPC . En particular, IPC no es estructuralmente completo.

• La regla

${\displaystyle {\frac {\Box p}{p}}}$

es admisible en muchas lógicas modales, como K , D , K 4 , S 4 , GL (consulte esta tabla para conocer los nombres de las lógicas modales). Es derivable en S 4 , pero no es derivable en K , D , K 4 o GL .

• La regla

${\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}}$

es admisible en lógica normal . ^[8] Es derivable en GL y S 4.1, pero no es derivable en K , D , K 4, S 4 o S 5. ${\displaystyle L\supseteq S4.3}$

• Regla de Löb

${\displaystyle ({\mathit {LR}})\qquad {\frac {\Box p\to p}{p}}}$

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, no es cierto en general que una regla admisible en una lógica L deba 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 . Nótese que el problema no es trivial incluso si la lógica misma (es decir, su conjunto de teoremas) es decidible : la definición de admisibilidad de una regla A / B involucra un cuantificador universal ilimitado sobre todas las sustituciones proposicionales. Por lo tanto , a priori solo sabemos que la admisibilidad de la 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 importante problema abierto. ${\displaystyle \Pi _{1}^{0}}$

Sin embargo, 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 ₀ , ... , p _k se llama reducida si tiene la forma

${\displaystyle {\frac {\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j=0}^{k}\neg _{i,j}^{0}p_{j}\land \bigwedge _{j=0}^{k}\neg _{i,j}^{1}\Box p_{j}{\bigr )}}{p_{0}}},}$

donde cada uno es un espacio en blanco o una 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 derive) s , introduciendo 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. ${\displaystyle \neg _{i,j}^{u}}$ ${\displaystyle \neg }$

Sea una regla reducida como la anterior. Identificamos cada conjunción con el conjunto de sus conjunciones. Para cualquier subconjunto W del conjunto de todas las conjunciones, definamos un modelo de Kripke mediante ${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$ ${\displaystyle \varphi _{i}}$ ${\displaystyle \{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}}$ ${\displaystyle \{\varphi _{i}\mid i\leq n\}}$ ${\displaystyle M=\langle W,R,{\Vdash }\rangle }$

${\displaystyle \varphi _{i}\Vdash p_{j}\iff p_{j}\in \varphi _{i},}$

${\displaystyle \varphi _{i}\,R\,\varphi _{i'}\iff \forall j\leq k\,(\Box p_{j}\in \varphi _{i}\Rightarrow \{p_{j},\Box p_{j}\}\subseteq \varphi _{i'}).}$

A continuación se presenta un criterio algorítmico de admisibilidad en K 4: ^[13]

Teorema . La regla no es admisible en K 4 si y sólo si existe un conjunto tal que ${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$ ${\displaystyle W\subseteq \{\varphi _{i}\mid i\leq n\}}$

1. ${\displaystyle \varphi _{i}\nVdash p_{0}}$Para algunos ${\displaystyle i\leq n,}$
2. ${\displaystyle \varphi _{i}\Vdash \varphi _{i}}$Para cada uno ${\displaystyle i\leq n,}$
3. para cada subconjunto D de W existen elementos tales que las equivalencias ${\displaystyle \alpha ,\beta \in W}$

${\displaystyle \alpha \Vdash \Box p_{j}}$si y solo si para cada ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ ${\displaystyle \varphi \in D}$

${\displaystyle \alpha \Vdash \Box p_{j}}$si y solo si y para cada ${\displaystyle \alpha \Vdash p_{j}}$ ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ ${\displaystyle \varphi \in D}$

válido para todos los j .

Se pueden encontrar criterios similares para las lógicas S 4 , GL y Grz . ^[14] Además, la admisibilidad en lógica intuicionista se puede reducir a la admisibilidad en Grz utilizando la traducción de Gödel–McKinsey–Tarski : ^[15]

${\displaystyle A\,|\!\!\!\sim _{IPC}B}$Si y sólo si ${\displaystyle T(A)\,|\!\!\!\sim _{Grz}T(B).}$

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ógicas transitivas (es decir, que extienden K 4 o IPC ) modales y superintuicionistas, incluyendo, por ejemplo, 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 ). ^[16]

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 debe 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 lógicas proposicionales 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 el lenguaje de una lógica L (un L -unificador 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

${\displaystyle \vdash _{L}\sigma p\leftrightarrow \upsilon \tau p}$

para cada variable p . Un conjunto completo de unificadores de una fórmula A es un conjunto S de L -unificadores de A tal que cada L -unificador de A es menos general que algún unificador de S . Un unificador más general (MGU) de A es un unificador σ tal que { σ } es un conjunto completo de unificadores de A . De ello se deduce que si S es un conjunto completo de unificadores de A , entonces una regla A / B es L -admisible si y solo si cada σ en S es un L -unificador de B . Por tanto, podemos caracterizar 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 : son fórmulas A tales que existe un unificador σ de A tal que

${\displaystyle A\vdash _{L}B\leftrightarrow \sigma B}$

para cada fórmula B . Nótese que σ es una MGU de A . En lógicas transitivas modales y superintuicionistas con la propiedad de modelo finito , se pueden caracterizar las fórmulas proyectivas semánticamente como aquellas cuyo conjunto de L -modelos finitos tiene la propiedad de extensión : ^[19] si M es un L -modelo de Kripke finito 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 de modo que A sea verdadera también en r . Además, la prueba proporciona una construcción explícita de una MGU para una fórmula proyectiva dada A .

En las lógicas transitivas básicas IPC , K 4 , S 4 , GL , Grz (y más generalmente en cualquier lógica transitiva con la propiedad de modelo finito cuyo conjunto de marco finito satisface otro tipo de propiedad de extensión), podemos construir efectivamente para cualquier fórmula A su aproximación proyectiva Π( A ): ^[20] un conjunto finito de fórmulas proyectivas tales que

1. ${\displaystyle P\vdash _{L}A}$Para cada uno ${\displaystyle P\in \Pi (A),}$
2. Todo unificador de A es un unificador de una fórmula de Π( A ).

De ello se deduce que el conjunto de MGU de elementos de Π( A ) es un conjunto completo de unificadores de A . Además, si P es una fórmula proyectiva, entonces

${\displaystyle P\,|\!\!\!\sim _{L}B}$Si y sólo si ${\displaystyle P\vdash _{L}B}$

para cualquier fórmula B . De este modo obtenemos la siguiente caracterización efectiva de las reglas admisibles: ^[21]

${\displaystyle A\,|\!\!\!\sim _{L}B}$Si y sólo si ${\displaystyle \forall P\in \Pi (A)\,(P\vdash _{L}B).}$

Bases de las normas admisibles

Sea L una lógica. Un conjunto R de L -reglas admisibles se denomina base ^[22] de reglas admisibles, si cada regla admisible Γ/ B puede derivarse de R y de las reglas derivables de L , utilizando 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 . ${\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}}$ ${\displaystyle \vdash _{L}}$

Nótese que la decidibilidad de 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 correcursivamente enumerable, y si además tenemos una base recursivamente enumerable, el conjunto de reglas admisibles también es recursivamente enumerable; 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 unifique A pero no B , y otra para una derivación de A / B a partir de R y . Una de las búsquedas tiene que llegar eventualmente a una respuesta). Aparte de la decidibilidad, las bases explícitas de reglas admisibles son útiles para algunas aplicaciones, por ejemplo, en la complejidad de la prueba . ^[23] ${\displaystyle \vdash _{L}}$

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, puede tener, no obstante, 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 se comportan generalmente bien y siempre son finitamente axiomatizables, existen lógicas modales tabulares sin una base finita o independiente de reglas. ^[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 L -reglas admisibles si y sólo si L es estructuralmente completo.
• Toda extensión de la lógica modal S 4.3 (incluida, en particular, S 5) tiene una base finita que consiste en la regla única ^[27]

${\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}.}$

• Reglas de Visser  [nl]

${\displaystyle {\frac {\displaystyle {\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{n+1}\lor p_{n+2}{\Bigr )}\lor r}{\displaystyle \bigvee _{j=1}^{n+2}{\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{j}{\Bigr )}\lor r}},\qquad n\geq 1}$

son una base de reglas admisibles en el Código Penal de la India o en el Código de Contabilidad del Canadá . ^[28]

• Las reglas

${\displaystyle {\frac {\displaystyle \Box {\Bigl (}\Box q\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (q\land \Box q\to p_{i})\lor r}},\qquad n\geq 0}$

son una base de reglas admisibles de GL . ^[29] (Nótese que la disyunción vacía se define como .) ${\displaystyle \bot }$

• Las reglas

${\displaystyle {\frac {\displaystyle \Box {\Bigl (}\Box (q\to \Box q)\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (\Box q\to p_{i})\lor r}},\qquad n\geq 0}$

son una base de 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 verdadero para cada valoración en F : ${\displaystyle F=\langle W,R\rangle }$ ${\displaystyle \Vdash }$

Si para todos , entonces . ${\displaystyle A\in \Gamma }$ ${\displaystyle \forall x\in W\,(x\Vdash A)}$ ${\displaystyle \forall x\in W\,(x\Vdash B)}$

(La definición se puede generalizar fácilmente a marcos generales , si es necesario).

Sea X un subconjunto de W y t un punto en W. Decimos que t es

• un predecesor reflexivo estricto de X , si para cada y en W : t R y si y solo si t = y o para algún x en X : x = y o x R y ,
• un predecesor estricto irreflexivo de X , si para cada y en W : t R y si y sólo si para algún x en X : x = y o x R y .

Decimos que un marco F tiene predecesores estrictos reflexivos (irreflexivos), si para cada subconjunto finito X de W , existe un predecesor estricto reflexivo (irreflexivo) de X en W.

Tenemos: ^[31]

• una regla es admisible en el CPI si y sólo si es válida en todos los marcos intuicionistas que tienen predecesores reflexivos estrictos,
• una regla es admisible en K 4 si y sólo si es válida en todos los marcos transitivos que tienen predecesores estrictos reflexivos e irreflexivos,
• una regla es admisible en S 4 si y sólo si es válida en todos los marcos reflexivos transitivos que tienen predecesores reflexivos estrictos,
• una regla es admisible en GL si y sólo si es válida en todos los marcos transitivos inversos bien fundados que tienen predecesores estrictos irreflexivos.

Obsérvese que, salvo algunos casos triviales, los marcos con predecesores estrictos deben ser infinitos. Por lo tanto, las reglas admisibles en lógicas transitivas básicas no gozan de la propiedad de modelo finito.

Completitud estructural

Si bien una clasificación general de lógicas estructuralmente completas no es una tarea fácil, tenemos una buena comprensión 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 implicación admisible en una lógica superintuicionista es derivable. ^[32] Por otra parte, la regla de Mints

${\displaystyle {\frac {(p\to q)\to p\lor r}{((p\to q)\to p)\lor ((p\to q)\to r)}}}$

es admisible en la lógica intuicionista pero no derivable, y sólo contiene implicaciones y disyunciones.

Conocemos las lógicas transitivas estructuralmente máximas incompletas. Una lógica se denomina hereditariamente estructuralmente completa 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 las lógicas modales superintuicionistas y transitivas estructuralmente completas respectivamente. Es decir, una lógica superintuicionista es hereditariamente estructuralmente completa si y solo si no es válida en ninguno 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 ninguno de ciertos veinte marcos de Kripke (incluidos los cinco marcos intuicionistas anteriores). ^[9]

Existen lógicas estructuralmente completas que no son hereditariamente estructuralmente completas: 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

${\displaystyle {\frac {A(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}{B(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}},}$

cuyas variables se dividen en las variables "regulares" p _i , y los parámetros s _i . La regla es L -admisible si cada L -unificador σ de A tal que σs _i  =  s _i para cada i es también 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, escritos como

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B_{1},\dots ,B_{m}}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B_{1},\dots ,B_{m}.}$

Una regla de este tipo es admisible si cada unificador de Γ es también unificador de alguna fórmula a partir de Δ. ^[35] Por ejemplo, una lógica L es consistente si admite la regla

${\displaystyle {\frac {\;\bot \;}{}},}$

y una lógica superintuicionista tiene la propiedad de disyunción si y solo si admite la regla

${\displaystyle {\frac {p\lor q}{p,q}}.}$

Nuevamente, los resultados básicos sobre 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

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{\Box B_{1}\lor \dots \lor \Box B_{m}}}.}$

Sin embargo, a menudo se pueden emplear reglas de conclusiones múltiples para simplificar los argumentos.

En la teoría de la demostración , la admisibilidad se considera a menudo en el contexto de los cálculos secuenciales , donde los objetos básicos son secuenciales 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 cortes

${\displaystyle {\frac {\Gamma \vdash A,\Delta \qquad \Pi ,A\vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}.}$

(Por abuso del lenguaje, a veces también se dice que el cálculo secuente (completo) admite cortes, es decir, su versión sin cortes sí lo hace.) Sin embargo, la admisibilidad en cálculos secuentes suele ser solo una variante notacional para la admisibilidad en la lógica correspondiente: cualquier cálculo completo para (por ejemplo) lógica intuicionista admite una regla secuente si y solo si IPC admite la regla de fórmula que obtenemos al traducir cada secuente a su fórmula característica . ${\displaystyle \Gamma \vdash \Delta }$ ${\displaystyle \bigwedge \Gamma \to \bigvee \Delta }$

Notas

1. Blok y Pigozzi (1989), Kracht (2007)
2. Rybakov (1997), Definición 1.1.3
3. Rybakov (1997), Definición 1.7.2
4. Del teorema de De Jongh a la lógica intuicionista de las demostraciones
5. Rybakov (1997), Definición 1.7.7
6. Chagrov y Zakharyaschev (1997), Thm. 1.25
7. Prucnal (1979), véase Iemhoff (2006)
8. Rybakov (1997), pág. 439
9. Rybakov (1997), Tesis 5.4.4, 5.4.8
10. Cintula y Metcalfe (2009)
11. Wolter y Zakharyaschev (2008)
12. Rybakov (1997), §3.9
13. Rybakov (1997), Teoría 3.9.3
14. Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf. Chagrov y Zakharyaschev (1997), §16.7
15. Rybakov (1997), Teoría 3.2.2
16. Rybakov (1997), §3.5
17. Jerábek (2007)
18. Chagrov y Zakharyaschev (1997), §18.5
19. Ghilardi (2000), Teoría 2.2
20. Ghilardi (2000), pág. 196
21. Ghilardi (2000), Teoría 3.6
22. Rybakov (1997), Definición 1.4.13
23. Mentas y Kojevnikov (2004)
24. Rybakov (1997), Teoría 4.5.5
25. Rybakov (1997), §4.2
26. Jerábek (2008)
27. Rybakov (1997), Cor. 4.3.20
28. Iemhoff (2001, 2005), Rozière (1992)
29. Jerábek (2005)
30. Jerábek (2005, 2008)
31. Iemhoff (2001), Jeřábek (2005)
32. Rybakov (1997), Tesis 5.5.6, 5.5.9
33. Prucnal (1976)
34. Rybakov (1997), §6.1
35. Jeřábek (2005); cf. Kracht (2007), §7
36. Jeřábek (2005, 2007, 2008)

Referencias

• W. Blok, D. Pigozzi, Lógicas algebraizables , Memorias de la American Mathematical Society 77 (1989), núm. 396, 1989.
• A. Chagrov y M. Zakharyaschev, Lógica modal , 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), n.º 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), núm. 2, págs. 859-880. Proyecto Euclid JSTOR
• S. Ghilardi, Mejor solución de ecuaciones modales , Annals of Pure and Applied Logic 102 (2000), n.º 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), núm. 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), núm. 1, págs. 65–81. doi :10.1305/ndjfl/1107220674
• R. Iemhoff, Sobre las reglas de las lógicas intermedias , Archive for Mathematical Logic , 45 (2006), núm. 5, págs. 581–599. doi :10.1007/s00153-006-0320-8
• E. Jeřábek, Reglas admisibles de lógicas modales , Journal of Logic and Computation 15 (2005), n.º 4, págs. 411–431. doi :10.1093/logcom/exi029
• E. Jeřábek, Complejidad de reglas admisibles , Archive for Mathematical Logic 46 (2007), núm. 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), núm. 3, págs. 249–267. doi :10.1093/jigpal/jzn004
• M. Kracht, Modal Consequence Relations , en: Handbook of Modal Logic (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 operative Logik und Mathematik , Grundlehren der mathematischen 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. PD comprimido con g
• T. Prucnal, Completitud estructural del cálculo proposicional de Medvedev , Informes sobre lógica matemática 6 (1976), págs. 103-105.
• T. Prucnal, Sobre dos problemas de Harvey Friedman , Studia Logica 38 (1979), núm. 3, págs. 247–262. doi :10.1007/BF00405383
• P. Rozière, Reglas admisibles en cálculo proposicional intuitionniste , Ph.D. tesis, Universidad de París 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), n.º 4, artículo n.º 25. doi :10.1145/1380572.1380574 PDF