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

Definiciones

La admisibilidad se ha estudiado sistemáticamente sólo en el caso de reglas estructurales (es decir, de sustitución cerrada) en lógica proposicional no clásica , que describiremos a continuación.

Sea fijo un conjunto de conectivos proposicionales básicos (por ejemplo, en el caso de las lógicas superintuicionistas , o en el caso de las lógicas monomodales ). Las fórmulas bien formadas se construyen libremente utilizando estos conectivos de un conjunto infinitamente numerable de variables proposicionales p ₀ , p ₁ , .... Una sustitución σ es una función de fórmula a fórmula 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 consecuencias al estilo de 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 llama estructural . (Tenga en cuenta que el término "estructural" tal como se usa 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 llama 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. Un ejemplo 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 caso 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. (Tenga en cuenta que es una relación de consecuencia estructural por sí sola). ${\displaystyle \vdash }$ ${\displaystyle \Gamma \vdash B}$ ${\displaystyle \Gamma \mathrel {|\!\!\!\sim } B}$ ${\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}$

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

En lógicas con una conjunción conectiva de buen comportamiento (como la lógica superintuicionista o modal), una regla es equivalente a con respecto a la admisibilidad y la derivabilidad. Por lo tanto, es habitual tratar únicamente 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 fije una asignación v tal que v ( A ) = 1 y v ( 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 norma A / B tampoco es admisible. (El mismo argumento se aplica a cualquier lógica multivaluada L completa con respecto a una matriz lógica, todos cuyos elementos tienen 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 la premisa )

${\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 ( IPC ). De hecho, es admisible en toda lógica superintuicionista. ^[7] Por otro lado, 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, la IPC no está estructuralmente completa.

• 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 ver 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 lob

${\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 . Obsérvese 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 implica un cuantificador universal ilimitado sobre todas las sustituciones proposicionales. Por tanto, a priori sólo sabemos que la admisibilidad de una 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. Rybakov construyó los primeros procedimientos de decisión para reglas admisibles en lógicas modales transitivas básicas, utilizando la forma reducida de reglas . ^[12] Una regla modal en 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 está en blanco o en negación . Para cada regla r , podemos construir efectivamente una regla reducida s (llamada forma reducida de r ) tal que cualquier lógica admita (o derive) r si y sólo 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 tanto, basta con 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 por ${\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'}).}$

Entonces lo siguiente proporciona un criterio algorítmico para la 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 ${\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 sólo si y para cada ${\displaystyle \alpha \Vdash p_{j}}$ ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ ${\displaystyle \varphi \in D}$

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 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 solo 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 modales y superintuicionistas transitivas (es decir, que extienden K 4 o IPC ), incluidas, 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 ). ^[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 la lógica transitiva básica 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ó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 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 sólo 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 : estas 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 . Tenga en cuenta que σ es una MGU de A. En lógicas transitivas modales y superintuicionistas con la propiedad del modelo finito , se pueden caracterizar semánticamente las fórmulas proyectivas como aquellas cuyo conjunto de L -modelos finitos tiene la propiedad de extensión : ^[19] si M es un modelo L 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 en r , entonces podemos cambiar la valoración de las variables en r para que A también sea verdadera 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 del 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 ${\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 solo si ${\displaystyle P\vdash _{L}B}$

para cualquier fórmula B . Así obtenemos la siguiente caracterización efectiva de reglas admisibles: ^[21]

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

Bases de reglas admisibles

Sea L una lógica. Un conjunto R de L -reglas admisibles se llama 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 sólo 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 siempre es corresivamente enumerable, y si además tenemos una base recursivamente enumerable, el conjunto de reglas admisibles también es recursivamente enumerable; por 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). Además de la capacidad de decisión, 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 sin embargo 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, si bien las lógicas tabulares generalmente se comportan bien y siempre son finitamente axiomatizables, existen lógicas modales tabulares 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 L -reglas admisibles si y sólo 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 una 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 IPC o KC . ^[28]

• Las normas

${\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] (Tenga en cuenta que la disyunción vacía se define como ). ${\displaystyle \bot }$

• Las normas

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

si es 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 generaliza fácilmente a marcos generales , si es necesario).

Sea X un subconjunto de W y t un punto en W. Decimos que 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 irreflexivo y estricto 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 IPC 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 fundamentados que tienen predecesores irreflexivos estrictos.

Tenga en cuenta que, salvo algunos casos triviales, los fotogramas con predecesores ajustados deben ser infinitos. Por tanto, las reglas admisibles en lógica transitiva básica 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, conocemos bien 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 Mints

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

es admisible en 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 hereditariamente 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, respectivamente, una descripción completa de las lógicas modales superintuicionistas y transitivas hereditariamente estructuralmente completas. Es decir, una lógica superintuicionista es hereditariamente estructuralmente completa si y sólo 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 sólo 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 lo son estructuralmente 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

${\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 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 conclusiones múltiples 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}.}$

Tal regla es admisible si todo unificador de Γ es también un unificador de alguna fórmula 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 admite la regla

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

Nuevamente, los resultados básicos sobre reglas admisibles se generalizan fácilmente a reglas de conclusiones múltiples. ^[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 prueba , la admisibilidad a menudo se considera en el contexto de los cálculos sucesivos , donde los objetos básicos son consecuentes en lugar de fórmulas. Por ejemplo, se puede reformular el teorema de eliminación de cortes diciendo que el cálculo del secuente sin cortes admite la regla de corte

${\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 secuencial (completo) admite corte, es decir, su versión sin cortes sí lo admite.) Sin embargo, la admisibilidad en los cálculos secuenciales suele ser sólo una variante notacional de la admisibilidad en la lógica correspondiente: cualquier El cálculo completo para (digamos) la lógica intuicionista admite una regla del secuente si y sólo si IPC admite la regla de la 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), Def. 1.1.3
3. Rybakov (1997), Def. 1.7.2
4. Del teorema de de Jongh a la lógica intuicionista de las pruebas
5. Rybakov (1997), Def. 1.7.7
6. Chagrov y Zakharyaschev (1997), Thm. 1.25
7. Prucnal (1979), cf. Iemhoff (2006)
8. Rybakov (1997), pág. 439
9. Rybakov (1997), Thms. 5.4.4, 5.4.8
10. Cintula y Metcalfe (2009)
11. Wolter y Zakharyaschev (2008)
12. Rybakov (1997), §3.9
13. Rybakov (1997), Thm. 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), Thm. 3.2.2
16. Rybakov (1997), §3.5
17. Jeřábek (2007)
18. Chagrov y Zakharyaschev (1997), §18.5
19. Ghilardi (2000), Thm. 2.2
20. Ghilardi (2000), pág. 196
21. Ghilardi (2000), Thm. 3.6
22. Rybakov (1997), Def. 1.4.13
23. Mentas y Kojevnikov (2004)
24. Rybakov (1997), Thm. 4.5.5
25. Rybakov (1997), §4.2
26. Jeřábek (2008)
27. Rybakov (1997), Cor. 4.3.20
28. Iemhoff (2001, 2005), Rozière (1992)
29. Jeřábek (2005)
30. Jeřábek (2005, 2008)
31. Iemhoff (2001), Jeřábek (2005)
32. Rybakov (1997), Thms. 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 Sociedad Matemática Estadounidense 77 (1989), núm. 396, 1989.
• A. Chagrov y M. Zakharyaschev, Lógica modal , Guías de lógica de Oxford 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 Euclides 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), núm. 1, págs. 281–294. Proyecto Euclides JSTOR
• R. Iemhoff, Lógicas intermedias 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 la lógica intermedia , Archivo de Lógica Matemática , 45 (2006), núm. 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 reglas admisibles , Archivo de Lógica Matemática 46 (2007), no. 2, págs. 73–92. doi :10.1007/s00153-006-0028-9
• E. Jeřábek, Bases independientes de reglas admisibles , Revista Lógica de la 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 , Reports on Mathematical Logic 6 (1976), págs.
• 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 de descripción , ACM Transactions on Computational Logic 9 (2008), no. 4, artículo n. 25.doi :10.1145/1380572.1380574 PDF