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

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

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

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

${\displaystyle \сигма f(A_{1},\точки,A_{n})=f(\сигма A_{1},\точки,\сигма A_{n})}$

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

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

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

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

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

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

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

${\displaystyle \сигма A_{1},\точки,\сигма A_{n}/\сигма B}$

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

Каждое выводимое правило допустимо, но не наоборот в общем случае. Логика структурно полна, если каждое допустимое правило выводимо, т.е. . ^[5]${\displaystyle {\vdash }={\,|\!\!\!\sim }}$

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

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

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

допустимо в интуиционистском пропозициональном исчислении ( ИПС ). Фактически, оно допустимо в любой суперинтуиционистской логике. ^[7] С другой стороны, формула

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

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

• Правило

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

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

• Правило

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

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

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

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

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

• Логика Гёделя –Даммета ( LC ) и модальная логика Grz .3 являются структурно полными. ^[9] Нечеткая логика произведения также является структурно полной. ^[10]

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

Тем не менее, известно, что допустимость правил разрешима во многих модальных и суперинтуиционистских логиках. Первые процедуры принятия решений для допустимых правил в базовых транзитивных модальных логиках были построены Рыбаковым с использованием редуцированной формы правил . ^[12] Модальное правило от переменных p ₀ , ... , p _k называется редуцированным, если оно имеет вид

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

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

Пусть будет приведенным правилом, как указано выше. Мы отождествляем каждую конъюнкцию с множеством ее конъюнктов. Для любого подмножества W множества всех конъюнкций определим модель Крипке следующим образом:${\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'}).}$

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

Теорема . Правило недопустимо в K 4 тогда и только тогда , когда существует множество такое, что${\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}}$для некоторых${\displaystyle i\leq n,}$
2. ${\displaystyle \varphi _{i}\Vdash \varphi _{i}}$для каждого${\displaystyle i\leq n,}$
3. для каждого подмножества D из W существуют элементы, такие что эквивалентности${\displaystyle \alpha ,\beta \in W}$

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

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

справедливо для всех j .

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

${\displaystyle A\,|\!\!\!\sim _{IPC}B}$если и только если${\displaystyle 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 ). ^[16]

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

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

${\displaystyle \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, такой что

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

для каждой формулы B . Обратите внимание, что σ является МГУ A . В транзитивных модальных и суперинтуиционистских логиках со свойством конечной модели можно семантически охарактеризовать проективные формулы как те, набор конечных L -моделей которых имеет свойство расширения : ^[19] если M является конечной L -моделью Крипке с корнем r , кластер которого является синглетоном , и формула A верна во всех точках M , за исключением r , то мы можем изменить оценку переменных в r так, чтобы сделать A истинной и в r . Более того, доказательство дает явное построение МГУ для заданной проективной формулы A .

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

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

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

${\displaystyle P\,|\!\!\!\sim _{L}B}$если и только если${\displaystyle P\vdash _{L}B}$

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

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

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

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

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

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

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

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

• Правила Виссера  [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}$

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

• Правила

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

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

• Правила

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

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

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

если для всех , то .${\displaystyle A\in \Gamma }$ ${\displaystyle \forall x\in W\,(x\Vdash A)}$${\displaystyle \forall x\in W\,(x\Vdash B)}$

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

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

• рефлексивный плотный предшественник 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.

У нас есть: ^[31]

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

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

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

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

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

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

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

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

Существуют структурно полные логики, которые не являются наследственно структурно полными: например, логика Медведева структурно полна, ^[33] но она входит в структурно неполную логику KC .

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

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

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

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

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

Такое правило допустимо, если каждый объединитель Γ является также объединителем некоторой формулы из Δ. ^[35] Например, логика L непротиворечива , если и только если она допускает правило

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

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

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

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

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

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

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

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

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

• В. Блок, Д. Пигоцци, Алгебраизуемые логики , Мемуары Американского математического общества 77 (1989), № 396, 1989.
• А. Чагров и М. Захарьящев, Модальная логика , Oxford Logic Guides т. 35, Oxford University Press, 1997. ISBN  0-19-853779-4
• П. Синтула и Г. Меткалф, Структурная полнота в нечетких логиках , Notre Dame Journal of Formal Logic 50 (2009), № 2, стр. 153–182. doi :10.1215/00294527-2009-004
• А.И. Циткин, О структурно полных суперинтуиционистских логиках , Советская математика - Доклады, т. 19 (1978), с. 816–819.
• S. Ghilardi, Унификация в интуиционистской логике , Журнал символической логики 64 (1999), № 2, стр. 859–880. Проект Euclid JSTOR
• S. Ghilardi, Лучшее решение модальных уравнений , Annals of Pure and Applied Logic 102 (2000), № 3, стр. 183–198. doi :10.1016/S0168-0072(99)00032-9
• Р. Йемхофф , О допустимых правилах интуиционистской пропозициональной логики , Журнал символической логики 66 (2001), № 1, стр. 281–294. Проект Евклид JSTOR
• Р. Йемхофф, Промежуточные логики и правила Виссера , Notre Dame Journal of Formal Logic 46 (2005), № 1, стр. 65–81. doi :10.1305/ndjfl/1107220674
• Р. Иемхофф, О правилах промежуточной логики , Архив математической логики , 45 (2006), № 5, стр. 581–599. doi :10.1007/s00153-006-0320-8
• Э. Ержабек, Допустимые правила модальной логики , Журнал логики и вычислений 15 (2005), № 4, стр. 411–431. doi :10.1093/logcom/exi029
• Э. Ержабек, Сложность допустимых правил , Архив математической логики 46 (2007), № 2, стр. 73–92. doi :10.1007/s00153-006-0028-9
• Э. Ержабек, Независимые основания допустимых правил , Logic Journal of the IGPL 16 (2008), № 3, стр. 249–267. doi :10.1093/jigpal/jzn004
• M. Kracht, Modal Consequence Relations , в: Handbook of Modal Logic (P. Blackburn, J. van Benthem, and F. Wolter, eds.), Studies of Logic and Practical Reasoning, т. 3, Elsevier, 2007, стр. 492–545. ISBN 978-0-444-51690-9 
• П. Лоренцен, Einführung in die оперативной логике и математике , Grundlehren der mathematischen Wissenschaften vol. 78, Спрингер-Верлаг, 1955.
• Минц Г., Кожевников А., Интуиционистские системы Фреге полиномиально эквивалентны , Записки научных семинаров ПОМИ 316 (2004), стр. 129–146. сжатый PS
• Т. Прукнал, Структурная полнота исчисления высказываний Медведева , Отчеты по математической логике 6 (1976), стр. 103–105.
• T. Prucnal, О двух проблемах Харви Фридмана , Studia Logica 38 (1979), № 3, стр. 247–262. doi :10.1007/BF00405383
• П. Розьер, «Правила, допустимые в интуитивных вычислениях» , доктор философии. диссертация, Парижский университет VII , 1992. PDF
• В. В. Рыбаков, Допустимость правил логического вывода , Исследования по логике и основаниям математики, т. 136, Elsevier, 1997. ISBN 0-444-89505-1 
• Ф. Вольтер, М. Захарьящев, Неразрешимость проблем унификации и допустимости для модальных и дескриптивных логик , ACM Transactions on Computational Logic 9 (2008), № 4, статья № 25. doi :10.1145/1380572.1380574 PDF