Regla admisible

En lógica , una regla de inferencia es admisible en un sistema formal si el conjunto de teoremas del sistema no cambia al añadir dicha regla a las reglas ya existentes. En otras palabras, toda fórmula que pueda derivarse utilizando esa regla ya puede derivarse sin ella, por lo que, en cierto sentido, resulta redundante. El concepto de regla admisible fue introducido por Paul Lorenzen (1955).

La admisibilidad solo se ha estudiado sistemáticamente 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 conectores proposicionales básicos (por ejemplo,${\displaystyle \{\to ,\land ,\lor ,\bot \}}$en el caso de lógicas superintuicionistas , o${\displaystyle \{\to ,\bot ,\Box \}}$en el caso de lógicas monomodales ). Las fórmulas bien formadas se construyen libremente utilizando estos conectores 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 conectores, es decir,

${\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 al estilo Tarski ^{[ 1 ]} es una relación${\displaystyle \vdash }$entre conjuntos de fórmulas y fórmulas, de tal manera que

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

Para todas las sustituciones, σ se denomina estructural . (Nótese que el término "estructural", tal como se usa aquí y más adelante, no está relacionado con la noción de reglas estructurales en el cálculo de secuencias ). Una relación de consecuencia estructural se denomina lógica proposicional . Una fórmula A es un teorema de una lógica.${\displaystyle \vdash }$si${\displaystyle \varnothing \vdash A}$.

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

Una regla de inferencia estructural ^{[ 2 ]} (o simplemente regla para abreviar) viene dada por un par (Γ, B ), que normalmente se escribe como

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{o}}\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${\displaystyle \vdash }$, si${\displaystyle \Gamma \vdash B}$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, al añadirse a la lógica, no conduce a nuevos teoremas. ^{[ 4 ]} También escribimos${\displaystyle \Gamma \mathrel {|\!\!\!\sim } B}$si Γ/ B es admisible. (Tenga en cuenta que${\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}$es una relación de consecuencia estructural en sí misma.)

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

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

• 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 =${\displaystyle \top }$si v ( p ) = 1, y σp =${\displaystyle \bot }$Si v ( p ) = 0, entonces σA es un teorema, pero σB no lo es (de hecho, ¬σB sí lo es). 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 tengan nombre en el lenguaje de L ).
• La regla de Kreisel - Putnam (también conocida como regla de Harrop o regla de independencia de 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 ( 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 se puede derivar 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 (ver esta tabla para los nombres de las lógicas modales). Es derivable en S 4, pero no es derivable en K , D , K 4, ni GL .

• La regla

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

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

• La 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 de producto también es estructuralmente completa. ^{[ 10 ]}

La pregunta fundamental 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 implica un cuantificador universal no acotado sobre todas las sustituciones proposicionales. Por lo tanto, a priori solo sabemos que la admisibilidad de una regla en una lógica decidible es${\displaystyle \Pi _{1}^{0}}$(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 ]} Cabe destacar que la decidibilidad de la admisibilidad en la lógica modal básica K es un importante problema abierto .

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 las 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${\displaystyle \neg _ {i,j}^{u}}$está en blanco o es una negación.${\displaystyle \neg }$Para cada regla r , podemos construir una regla reducida s (denominada forma reducida de r ) de tal manera que cualquier lógica admita (o derive) r si y solo si admite (o deriva) 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, basta con construir un algoritmo de decisión para la admisibilidad de reglas reducidas.

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

${\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 proporciona un criterio algorítmico de admisibilidad en K 4: ^{[ 13 ]}

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

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

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

${\displaystyle \alpha \Vdash \Box p_{j}}$si y solo si${\displaystyle \alpha \Vdash p_{j}}$y${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$por cada${\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 la 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 demostrar 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 ), 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 , K4 , S4 , GL y 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 -completa. ^{[ 18 ]}

La admisibilidad en lógicas proposicionales está estrechamente relacionada con la unificación en la teoría ecuacional de álgebras modales o de Heyting . La conexión fue desarrollada por Ghilardi (1999, 2000). En el marco lógico, 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 "todo 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 lo tanto, podemos caracterizar las reglas admisibles si podemos encontrar conjuntos completos de unificadores bien comportados.

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. Nótese que σ es una MGU de A. En lógicas modales transitivas 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 clúster 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 sea verdadera también en r . Además, la demostración proporciona una construcción explícita de una MGU para una fórmula proyectiva A dada .

En las lógicas transitivas básicas IPC , K4 , S4 , 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}$por cada${\displaystyle P\in \Pi (A),}$
2. cada 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 las reglas admisibles: ^{[ 21 ]}

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

Sea L una lógica. Un conjunto R de reglas L -admisibles se denomina base ^{[ 22 ]} de reglas admisibles si toda 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${\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}}$es la relación de consecuencia estructural más pequeña que incluye${\displaystyle \vdash _{L}}$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 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 unifica A pero no B , y otra para una derivación de A / B a partir de R y${\displaystyle \vdash _{L}}$Una de las búsquedas debe eventualmente dar con una respuesta. Aparte de la decidibilidad, las bases explícitas de reglas admisibles son útiles para algunas aplicaciones, por ejemplo, en la complejidad de las pruebas . ^{[ 23 ]}

Para una lógica dada, podemos preguntarnos si posee una base recursiva o finita de reglas admisibles y proporcionar una base explícita. Si una lógica no tiene una base finita, puede, no obstante, 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 suelen comportarse 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 sí tienen bases independientes. ^{[ 26 ]}

Una regla Γ/ B es válida en un marco de Kripke modal o intuicionista.${\displaystyle F=\langle W,R\rangle }$, si lo siguiente es cierto para cada valoración${\displaystyle \Vdash }$en F :

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

(La definición se generaliza fácilmente a marcos generales , si fuera necesario).

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

• un predecesor estricto reflexivo 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 ajustado irreflexivo de X , si para cada y en W : t R y si y solo si para algún x en X : x = y o x R y .

We say that a frame F has reflexive (irreflexive) tight predecessors, if for every finite subset X of W, there exists a reflexive (irreflexive) tight predecessor of X in W.

We have:^[31]

• a rule is admissible in IPC if and only if it is valid in all intuitionistic frames that have reflexive tight predecessors,
• a rule is admissible in K4 if and only if it is valid in all transitive frames that have reflexive and irreflexive tight predecessors,
• a rule is admissible in S4 if and only if it is valid in all transitive reflexive frames that have reflexive tight predecessors,
• a rule is admissible in GL if and only if it is valid in all transitive converse well-founded frames that have irreflexive tight predecessors.

Note that apart from a few trivial cases, frames with tight predecessors must be infinite. Hence admissible rules in basic transitive logics do not enjoy the finite model property.

While a general classification of structurally complete logics is not an easy task, we have a good understanding of some special cases.

Intuitionistic logic itself is not structurally complete, but its fragments may behave differently. Namely, any disjunction-free rule or implication-free rule admissible in a superintuitionistic logic is derivable.^[32] On the other hand, the Mints rule

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

is admissible in intuitionistic logic but not derivable, and contains only implications and disjunctions.

We know the maximal structurally incomplete transitive logics. A logic is called hereditarily structurally complete, if any extension is structurally complete. For example, classical logic, as well as the logics LC and Grz.3 mentioned above, are hereditarily structurally complete. A complete description of hereditarily structurally complete superintuitionistic and transitive modal logics was given respectively by Citkin and Rybakov. Namely, a superintuitionistic logic is hereditarily structurally complete if and only if it is not valid in any of the five Kripke frames^[9]

Similarly, an extension of K4 is hereditarily structurally complete if and only if it is not valid in any of certain twenty Kripke frames (including the five intuitionistic frames above).^[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 .

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 todo 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 extienden 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

${\displaystyle {\frac {A_{1},\dots ,A_{n}}{B_{1},\dots ,B_{m}}}\qquad {\text{o}}\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 y solo 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 múltiples conclusiones. ^{[ 36 ]} En lógicas con una variante de la propiedad de disyunción, las reglas de múltiples conclusiones tienen el mismo poder expresivo que las reglas de una sola conclusión: 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, las reglas de conclusiones múltiples a menudo pueden emplearse para simplificar los argumentos.

En teoría de la demostración , la admisibilidad se considera a menudo en el contexto de los cálculos de secuentes , donde los objetos básicos son los secuentes en lugar de las fórmulas. Por ejemplo, se puede reformular el teorema de eliminación de cortes diciendo que el cálculo de secuentes 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, también se dice a veces que el cálculo de secuencias (completo) admite cortes, lo que significa que su versión sin cortes sí los admite). Sin embargo, la admisibilidad en los cálculos de secuencias suele ser solo una variante notacional de la admisibilidad en la lógica correspondiente: cualquier cálculo completo para (digamos) la lógica intuicionista admite una regla de secuencias si y solo si el IPC admite la regla de fórmula que obtenemos al traducir cada secuencia.${\displaystyle \Gamma \vdash \Delta }$a su fórmula característica${\displaystyle \bigwedge \Gamma \to \bigvee \Delta }$.

• Extensión mediante nuevos nombres de constantes y funciones.
• Extensión conservadora

• W. Blok, D. Pigozzi, Lógicas algebraizables , Memoirs of the American Mathematical Society 77 (1989), no. 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), pp.  816 – 819.
• S. Ghilardi, Unificación en lógica intuicionista , Journal of Symbolic Logic 64 (1999), n.º 2, págs.  859–880. Proyecto Euclid JSTOR
• S. Ghilardi, Mejor resolució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.º 1, págs.  281-294. Proyecto Euclid JSTOR
• R. Iemhoff, Lógicas intermedias y reglas de Visser , Notre Dame Journal of Formal Logic 46 (2005), n.º 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.º 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 las reglas admisibles , Archive for Mathematical Logic 46 (2007), n.º 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.º 3, págs.  249–267. doi : 10.1093/jigpal/jzn004
• M. Kracht, Relaciones de consecuencia modales , 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, pp.  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), pp.  103–105.
• T. Prucnal, Sobre dos problemas de Harvey Friedman , Studia Logica 38 (1979), n.º 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 en 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