Допустимое правило

Эта статья о правилах вывода в логических системах. Для понятия теории принятия решений см. допустимое правило принятия решения . О замене решения системы символьных уравнений см. Унификация (информатика) .

В логике правило вывода допустимо , в формальной системе если набор теорем системы не меняется при добавлении этого правила к существующим правилам системы. Другими словами, каждая формула , которая может быть выведена с использованием этого правила, уже выведена без этого правила, поэтому в некотором смысле она избыточна. Понятие допустимого правила было введено Полем Лоренценом (1955).

Определения

Допустимость систематически изучалась только в случае структурных (т. е. замкнутых подстановкой ) правил в пропозициональных неклассических логиках , которые мы опишем далее.

Пусть фиксирован набор основных пропозициональных связок (например, $\{\to ,\land ,\lor ,\bot \}$ в случае суперинтуиционистской логики , или $\{\to ,\bot ,\Box \}$ в случае мономодальных логик ). Правильно построенные формулы свободно строятся с использованием этих связок из счетного бесконечного набора пропозициональных переменных p ₀ , p ₁ , .... Замена σ - это функция от формул к формулам, которая коммутирует с применением связок, т. е.

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

для каждой связки f и формул A ₁ , ... An _, . (Мы также можем применять замены к множествам формул Γ, делая σ Γ = { σA : A ∈ Γ}. в стиле Тарского ) Отношение следствия это отношение $\vdash$ между наборами формул и формулами, такими что

1. $A\vdash A,$
2. если $\Gamma \vdash A$ затем $\Gamma ,\Delta \vdash A,$ («ослабление»)
3. если $\Gamma \vdash A$ и $\Delta ,A\vdash B$ затем $\Gamma ,\Delta \vdash B,$ («композиция»)

для всех формул A , B и наборов формул Γ, ∆. Отношение следствия такое, что

4. если $\Gamma \vdash A$ затем $\sigma \Gamma \vdash \sigma A$

для всех замен σ называется структурной . (Обратите внимание, что термин «структурный», используемый здесь и ниже, не имеет отношения к понятию структурных правил в секвенциальном исчислении .) Структурное отношение следствия называется логикой высказываний . Формула А — это теорема логики $\vdash$ если $\varnothing \vdash A$.

Например, мы отождествляем суперинтуиционистскую логику L с ее стандартным отношением следования $\vdash _{L}$ порождается modus ponens и аксиомами, и мы отождествляем нормальную модальную логику с ее глобальным отношением последствий $\vdash _{L}$ порождены modus ponens, необходимостью и (как аксиомы) теоремами логики.

Правило структурного вывода (или просто правило ) задается парой (Γ, B ), обычно записываемой как

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

{ A ₁ , ... , An _{где Γ =} } — конечное множество формул, а B — формула. Примером является правила

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

для замены σ . Правило Γ B выводится / в $\vdash$, если $\Gamma \vdash B$. Допустимо , если для каждого случая правила σB является теоремой, если все формулы из σΓ являются теоремами. Другими словами, правило допустимо, если оно при добавлении к логике не приводит к новым теоремам. Мы также пишем $\Gamma \mathrel {|\!\!\!\sim } B$ если Γ/ B допустима. (Обратите внимание, что ${\phantom {.}}\!{|\!\!\!\sim }$ само по себе является структурным отношением следствия.)

Любое выводимое правило допустимо, но не наоборот вообще. Логика является структурно полной, если каждое допустимое правило выводимо, т. е. ${\vdash }={\,|\!\!\!\sim }$.

В логиках с хорошей союзной связкой (например, в суперинтуиционистской или модальной логике) правило $A_{1},\dots ,A_{n}/B$ эквивалентно $A_{1}\land \dots \land A_{n}/B$ относительно допустимости и производности. Поэтому принято иметь дело только с унарными правилами A / B .

Примеры

• Классическое исчисление высказываний ( КПК ) структурно завершено. Действительно, предположим, что A / B — невыводимое правило, и зафиксируем присвоение v такое, что v ( A ) = 1 и v ( B ) = 0. Определим замену σ такую, что для каждой p переменной σp = $\top$ если v ( p ) = 1 и σp = $\bot$ если v ( p ) = 0. Тогда σA — теорема, а σB — нет (фактически, ¬ σB — теорема). Таким образом, правило A / B также недопустимо. (Тот же аргумент применим к любой многозначной логике L, полной относительно логической матрицы, все элементы которой имеют имя на языке L. )
• Правило Крейзеля правило – Патнэма (также известное как Харропа или правило независимости посылок )

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

допустимо в интуиционистском исчислении высказываний ( IPC ). Фактически, оно допустимо в любой суперинтуиционистской логике. С другой стороны, формула

$(\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))$

не является интуиционистской теоремой; следовательно, KPR не выводится в IPC . В частности, IPC не является структурно завершенным.

• Правило

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

допустимо во многих модальных логиках, таких как K , D , K 4, S 4, GL ( см. в этой таблице названия модальных логик ). Оно выводимо в S4 , но не выводимо в K , D , K4 или GL .

• Правило

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

допустимо в нормальной логике $L\supseteq S4.3$. Оно выводимо в GL и S 4.1, но не выводимо в K , D , K 4 , S 4 или S 5.

• Правило Лёба

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

допустимо (но не выводимо) в базовой модальной логике K и выводимо в GL . Однако LR недопустим в K 4. В частности, вообще говоря, неверно , что правило, допустимое в логике L, должно быть допустимым и в ее расширениях.

• Логика Гёделя-Даммета ( LC ) и модальная логика Grz .3 структурно полны. также Нечеткая логика продукта структурно завершена.

и

Основной вопрос о допустимых правилах данной логики состоит в том, разрешимо ли множество всех допустимых правил . Заметим, что проблема нетривиальна, даже если сама логика (т. е. ее набор теорем) разрешима : определение допустимости правила A / B включает в себя неограниченный квантор универсальности над всеми пропозициональными подстановками. Следовательно, априори мы знаем только, что допустимость правила в разрешимой логике равна $\Pi _{1}^{0}$ (т. е. его дополнение рекурсивно перечислимо ). Например, известно, что допустимость в бимодальных логиках K _u и K 4 _u (расширениях K или K 4 с универсальной модальностью ) неразрешима. Примечательно, что разрешимость допустимости в базовой модальной логике K является основной открытой проблемой.

Тем не менее, как известно, допустимость правил разрешима во многих модальных и суперинтуиционистских логиках. Первые процедуры решения допустимых правил в базовых транзитивных модальных логиках были построены Рыбаковым с использованием сокращенной формы правил . Модальное правило в переменных называется _вид приведенным , _p0,...,pk если оно имеет

${\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}}},$

где каждый $\neg _{i,j}^{u}$ либо пусто, либо отрицание $\neg$. Для каждого правила r мы можем эффективно построить сокращенное правило s (называемое приведенной формой r ), такое, что любая логика допускает (или выводит) r тогда и только тогда, когда она допускает (или выводит) s , путем введения переменных расширения для всех подформул. в A и выражая результат в полной дизъюнктивной нормальной форме . Таким образом, достаточно построить алгоритм принятия решения о допустимости сокращенных правил.

Позволять $\textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}$ быть сокращенным правилом, как указано выше. Мы идентифицируем каждое соединение $\varphi _{i}$ с набором $\{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}$ его конъюнктов. Для любого подмножества W множества $\{\varphi _{i}\mid i\leq n\}$ из всех конъюнкций определим модель Крипке $M=\langle W,R,{\Vdash }\rangle$ к

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

$\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'}).$

Тогда алгоритмический критерий допустимости в K 4 дает следующее:

Теорема . Правило $\textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}$ недопустима 4 тогда и только тогда , в K когда существует множество $W\subseteq \{\varphi _{i}\mid i\leq n\}$ такой, что

1. $\varphi _{i}\nVdash p_{0}$ для некоторых $i\leq n,$
2. $\varphi _{i}\Vdash \varphi _{i}$ для каждого $i\leq n,$
3. для любого подмножества D из W существуют элементы $\alpha ,\beta \in W$ такие, что эквивалентности

$\alpha \Vdash \Box p_{j}$ тогда и только тогда, когда $\varphi \Vdash p_{j}\land \Box p_{j}$ для каждого $\varphi \in D$

$\alpha \Vdash \Box p_{j}$ тогда и только тогда, когда $\alpha \Vdash p_{j}$ и $\varphi \Vdash p_{j}\land \Box p_{j}$ для каждого $\varphi \in D$

придерживаться для всех j .

Аналогичные критерии можно найти для логик S4 , GL и Grz . Более того, допустимость в интуиционистской логике может быть сведена к допустимости в Grz с использованием перевода Гёделя – МакКинси – Тарского :

$A\,|\!\!\!\sim _{IPC}B$ тогда и только тогда, когда $T(A)\,|\!\!\!\sim _{Grz}T(B).$

Рыбаков (1997) разработал гораздо более сложные методы демонстрации разрешимости допустимости, которые применимы к устойчивому (бесконечному) классу транзитивных (т. е. расширяющих K 4 или IPC ) модальных и суперинтуиционистских логик, включая, например, S 4.1, S 4.2, S 4.3. , KC , T _k (а также упомянутые выше логики IPC , K 4 , S 4 , GL , Grz ).

Несмотря на разрешимость, проблема допустимости имеет относительно высокую вычислительную сложность даже в простых логиках: допустимость правил в базовых транзитивных логиках IPC , K 4, S 4, GL , Grz является coNEXP -полной. Это следует противопоставить проблеме выводимости (для правил или формул) в этой логике, которая является PSPACE -полной.

Проективность и унификация

логике высказываний тесно связана с унификацией в эквациональной теории модальных Допустимость в или гейтинговых алгебр . Связь была разработана Гиларди (1999, 2000). В логической схеме унификатор формулы A на языке логики L ( L сокращенно -объединитель) представляет собой замену σ такую, что σA является теоремой L . (Используя это понятие, мы можем перефразировать допустимость правила A / B в L как «каждый L -объединитель A является L -объединителем B ».) L -объединитель σ менее общий, чем L -объединитель τ , записано как σ ≤ τ , если существует замена υ такая, что

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

для каждой переменной p . Полное множество объединителей формулы A — это множество S - объединителей L формулы A такое, что каждый L -объединитель формулы A менее общий, чем некоторый объединитель S. из Наиболее общий унификатор (MGU) A - это унификатор σ такой, что { σ } является полным набором унификаторов A . Отсюда следует, что если S — полный набор объединителей A , то правило A / B является L -допустимым тогда и только тогда, когда каждое в S является L - объединителем B. σ Таким образом, мы можем охарактеризовать допустимые правила, если сможем найти корректные полные наборы унификаторов.

Важным классом формул, имеющих наиболее общий объединитель, являются проективные формулы : это формулы A такие, что существует объединитель σ формулы A такой, что

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

для каждой B. формулы Обратите внимание, что σ является MGU A . В транзитивных модальных и суперинтуиционистских логиках со свойством конечной модели проективные формулы можно семантически охарактеризовать как те, у которых множество конечных L -моделей обладает свойством расширения : если M — конечная L -модель Крипке с корнем r , кластер которой представляет собой одноэлементный элемент , и формула A выполняется во всех точках M , кроме r , то мы можем изменить оценку переменных в r так, чтобы сделать A истинным в точке р тоже. Более того, доказательство дает явное построение MGU для заданной проективной формулы A .

В базовых транзитивных логиках IPC , K 4 , S 4 , GL , Grz (и, в более общем плане, в любой транзитивной логике со свойством конечной модели, множество конечного фрейма которой удовлетворяет другому типу свойства расширения), мы можем эффективно построить для любой формулы A его проективная аппроксимация Π( A ): конечное множество проективных формул таких, что

1. $P\vdash _{L}A$ для каждого $P\in \Pi (A),$
2. каждый объединитель A является объединителем формулы из Π( A ).

Отсюда следует, что множество MGU элементов из Π( A ) является полным набором объединителей A . Более того, если P — проективная формула, то

$P\,|\!\!\!\sim _{L}B$ тогда и только тогда, когда $P\vdash _{L}B$

для любой B. формулы Таким образом, мы получаем следующую эффективную характеристику допустимых правил:

$A\,|\!\!\!\sim _{L}B$ тогда и только тогда, когда $\forall P\in \Pi (A)\,(P\vdash _{L}B).$

Основы допустимых правил

Пусть L — логика. Множество R L . -допустимых правил называется базисом допустимых правил, если каждое допустимое правило Γ/ B может быть получено из R и выводимых правил L с помощью замены, композиции и ослабления. Другими словами, R является базисом тогда и только тогда, когда ${\phantom {.}}\!{|\!\!\!\sim _{L}}$ это наименьшее структурное отношение следствия, которое включает в себя $\vdash _{L}$ и Р. ​

Заметим, что разрешимость допустимых правил разрешимой логики эквивалентна существованию рекурсивных (или рекурсивно перечислимых ) базисов: с одной стороны, множество всех допустимых правил является рекурсивным базисом, если допустимость разрешима. С другой стороны, набор допустимых правил всегда корекурсивно перечислим, и если у нас дополнительно есть рекурсивно перечислимая основа, набор допустимых правил также будет рекурсивно перечислим; следовательно, это разрешимо. (Другими словами, мы можем решить допустимость A / B по следующему алгоритму : мы начинаем параллельно два исчерпывающих поиска : один для замены σ , которая объединяет A, но не B , и один для вывода A / B из R и $\vdash _{L}$. Один из поисков должен в конечном итоге дать ответ.) Помимо разрешимости, явные основы допустимых правил полезны для некоторых приложений, например, для сложности доказательства .

Для данной логики мы можем спросить, имеет ли она рекурсивный или конечный базис допустимых правил, и предоставить явный базис. Если логика не имеет конечного базиса, она, тем не менее, может иметь независимый базис : базис R такой, что ни одно собственное подмножество R не является базисом.

В общем, о существовании оснований с желаемыми свойствами можно сказать очень мало. Например, хотя табличные логики обычно хорошо себя ведут и всегда конечно аксиоматизируемы, существуют табличные модальные логики без конечной или независимой базы правил. Конечные базисы сравнительно редки: даже базисные транзитивные логики IPC , K4 , S4 , GL , Grz не имеют конечного базиса допустимых правил, хотя у них есть независимые базы.

Примеры баз

• Пустое множество является базисом L -допустимых правил тогда и только тогда, когда L структурно полно.
• Каждое расширение модальной логики S 4.3 (включая, в частности, S 5) имеет конечный базис, состоящий из единственного правила

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

• Visser Правила

${\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$

являются основой допустимых правил в МПК или КС .

• Правила

${\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$

являются основой допустимых правил GL . (Обратите внимание, что пустая дизъюнкция определяется как $\bot$.)

• Правила

${\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$

являются основой допустимых правил S 4 или Grz .

Семантика допустимых правил

Правило Γ/ B справедливо . в модальном или интуиционистском фрейме Крипке $F=\langle W,R\rangle$, если для каждой оценки верно следующее $\Vdash$ в Ф :

если для всех $A\in \Gamma$ $\forall x\in W\,(x\Vdash A)$, затем $\forall x\in W\,(x\Vdash B)$.

это определение легко обобщается на общие рамки ( При необходимости .)

Пусть X — подмножество W , а t — в W. точка Мы говорим, это что

• рефлексивный жесткий предшественник X или , если для каждого y в W : t R y тогда и только тогда, когда t = y для некоторого x в X : x = y или x R y ,
• иррефлексивный жесткий предшественник X тогда , если для каждого y в W : t R y и только тогда, когда для некоторого x в X : x = y или x R y .

Мы говорим, что фрейм F имеет рефлексивных (иррефлексивных) жестких предшественников, если для каждого конечного подмножества X из W существует рефлексивный (иррефлексивный) плотный предшественник X в W .

У нас есть:

• правило допустимо в IPC тогда и только тогда, когда оно действительно во всех интуиционистских фреймах, имеющих рефлексивных жестких предшественников,
• правило допустимо в K 4 тогда и только тогда, когда оно справедливо во всех транзитивных фреймах, имеющих рефлексивных и иррефлексивных жестких предшественников,
• правило допустимо в S4 тогда и только тогда, когда оно действительно во всех транзитивных рефлексивных фреймах, имеющих рефлексивных жестких предшественников,
• правило допустимо в GL тогда и только тогда, когда оно справедливо во всех транзитивных обратных хорошо обоснованных фреймах, имеющих иррефлексивных жестких предшественников.

Обратите внимание, что за исключением нескольких тривиальных случаев, кадры с плотными предшественниками должны быть бесконечными. Следовательно, допустимые правила в основных транзитивных логиках не обладают свойством конечной модели.

завершенность

Хотя общая классификация структурно полных логик — непростая задача, мы хорошо понимаем некоторые частные случаи.

Сама по себе интуиционистская логика структурно не завершена, но ее фрагменты могут вести себя по-разному. А именно, любое правило без дизъюнкций или правило без импликаций, допустимое в суперинтуиционистской логике, выводимо. С другой стороны, Минтов правила

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

допустима в интуиционистской логике, но невыводима и содержит только импликации и дизъюнкции.

Нам известны максимальные структурно неполные транзитивные логики. Логика называется наследственно структурно полной , если какое-либо расширение является структурно полным. Например, классическая логика, а также упомянутые выше логики LC и Grz.3 наследственно структурно полны. Полное описание наследственно структурно полной суперинтуиционистской и транзитивной модальных логик было дано соответственно Циткиным и Рыбаковым. А именно, суперинтуиционистская логика наследственно структурно полна тогда и только тогда, когда она недействительна ни в одной из пяти систем Крипке.

Аналогично, расширение K 4 является наследственно структурно полным тогда и только тогда, когда оно недействительно ни в одной из определенных двадцати систем Крипке (включая пять интуиционистских структур, упомянутых выше).

Существуют структурно полные логики, которые не являются наследственно структурно полными: например, логика Медведева структурно завершена, но оно включено в структурно неполную логику КС .

Варианты

Правило с параметрами — это правило вида

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

переменные которого разделены на «обычные» переменные и _pi параметры s _i . Правило является L если каждый L -объединитель σ A -допустимым , такой, что σs _i = s _i для каждого i, является также объединителем B . Основные результаты о разрешимости допустимых правил также относятся к правилам с параметрами.

Правило множественного вывода — это пара (Γ,Δ) двух конечных наборов формул, записанных как

${\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}.$

Такое правило допустимо, если каждый объединитель Г является также объединителем некоторой формулы из А. Например, логика L непротиворечива тогда и только тогда, когда она допускает правило

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

а суперинтуиционистская логика обладает свойством дизъюнкции тогда и только тогда, когда она допускает правило

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

Опять же, основные результаты о допустимых правилах плавно обобщаются на правила множественных выводов. В логиках с вариантом свойства дизъюнкции правила множественного вывода имеют ту же выразительную силу, что и правила одного вывода: например, в S 4 приведенное выше правило эквивалентно

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

Тем не менее, правила множественных выводов часто можно использовать для упрощения аргументов.

В теории доказательств допустимость часто рассматривается в контексте секвенциальных исчислений , где основными объектами являются секвенции, а не формулы. Например, можно перефразировать теорему об исключении разрезов , сказав, что секвенционное исчисление без разрезов допускает правило разреза.

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

(Злоупотребляя языком, иногда также говорят, что (полное) секвенциальное исчисление допускает разрез, то есть его версия без разрезов допускает.) Однако допустимость в секвенциальном исчислении обычно представляет собой лишь вариант обозначения допустимости в соответствующей логике: любой полное исчисление для (скажем) интуиционистской логики допускает правило секвенций тогда и только тогда, когда IPC допускает формульное правило, которое мы получаем путем перевода каждой секвенции $\Gamma \vdash \Delta$ к его характеристической формуле $\bigwedge \Gamma \to \bigvee \Delta$.

Ссылки

• В. Блок, Д. Пигоцци, Алгебраизуемая логика , Мемуары Американского математического общества 77 (1989), вып. 396, 1989.
• А. Чагров и М. Захарьящев, Модальная логика , Oxford Logic Guides vol. 35, Издательство Оксфордского университета, 1997. ISBN   0-19-853779-4
• П. Синтула и Г. Меткалф, Структурная полнота в нечеткой логике , Notre Dame Journal of Formal Logic 50 (2009), вып. 2, стр. 153–182. дои : 10.1215/00294527-2009-004
• А. И. Циткин, О структурно полной суперинтуиционистской логике , Советская математика - Доклады, вып. 19 (1978), стр. 816–819.
• С. Гиларди, Унификация в интуиционистской логике , Журнал символической логики 64 (1999), вып. 2, стр. 859–880. Проект Евклид JSTOR
• С. Гиларди, Лучшее решение модальных уравнений , Анналы чистой и прикладной логики 102 (2000), вып. 3, стр. 183–198. два : 10.1016/S0168-0072(99)00032-9
• Р. Иемхофф , О допустимых правилах интуиционистской пропозициональной логики , Журнал символической логики 66 (2001), вып. 1, стр. 281–294. Проект Евклид JSTOR
• Р. Иемхофф, Промежуточная логика и правила Виссера , Журнал формальной логики Нотр-Дам 46 (2005), вып. 1, стр. 65–81. два : 10.1305/ndjfl/1107220674
• Р. Иемхофф, О правилах промежуточной логики , Архив математической логики , 45 (2006), вып. 5, стр. 581–599. два : 10.1007/s00153-006-0320-8
• Е. Ержабек, Допустимые правила модальной логики , Журнал логики и вычислений 15 (2005), вып. 4, стр. 411–431. два : 10.1093/logcom/exi029
• Е. Ержабек, Сложность допустимых правил , Архив математической логики 46 (2007), вып. 2, стр. 73–92. два : 10.1007/s00153-006-0028-9
• Е. Ержабек, Независимые основы допустимых правил , Логический журнал IGPL 16 (2008), вып. 3, стр. 249–267. два : 10.1093/jigpal/jzn004
• М. Крахт, Модальные отношения последствий , в: Справочник по модальной логике (П. Блэкберн, Дж. ван Бентем и Ф. Вольтер, ред.), Исследования логики и практического рассуждения, том. 3, Elsevier, 2007, стр. 492–545. ISBN   978-0-444-51690-9
• П. Лоренцен, Введение в операционную логику и математику , Основы математических наук, том. 78, Спрингер Верлаг, 1955 г.
• G. Mints and A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent , Zapiski Nauchnyh Seminarov POMI 316 (2004), pp. 129–146. gzipped PS
• Т. Прунал, Структурная полнота исчисления высказываний Медведева , Отчеты по математической логике 6 (1976), стр. 103–105.
• Т. Прунал, О двух задачах Харви Фридмана , Studia Logica 38 (1979), вып. 3, стр. 247–262. два : 10.1007/BF00405383
• П. Розьер, Допустимые правила в интуиционистском исчислении высказываний , докторская диссертация, Парижский университет VII , 1992. PDF.
• В. В. Рыбаков, Допустимость правил логического вывода , Исследования по логике и основам математики вып. 136, Эльзевир, 1997. ISBN   0-444-89505-1
• Ф. Вольтер, М. Захарьящев, Неразрешимость проблем унификации и допустимости модальных и дескриптивных логик , Транзакции ACM по вычислительной логике 9 (2008), вып. 4, статья №. 25. дои : 10.1145/1380572.1380574 PDF