許容される規則

論理学において、推論規則は、その規則を既存の規則に追加しても、その体系の定理の集合が変化しない場合に、形式体系において許容される。言い換えれば、その規則を用いて導出できるすべての式は、その規則を用いなくても既に導出可能であるため、ある意味で冗長である。許容される規則の概念は、ポール・ローレンツェン（1955年）によって導入された。

許容性については、命題非古典論理における構造的（すなわち置換閉じた）規則の場合に限り体系的に研究されてきた。これについては次に説明する。

基本的な命題結合子のセットを固定します（例えば、${\displaystyle \{\to ,\land ,\lor ,\bot \}}$超直観主義論理の場合、または${\displaystyle \{\to ,\bot ,\Box \}}$（単一様論理の場合）。整形式論理式は、可算無限集合の命題変数p ₀、p ₁、 ...からこれらの結合子を使用して自由に構築されます。置換σは、結合子の適用と可換な論理式から論理式への関数です。

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

すべての結合子fと論理式A ₁ , ... , A _nに対して。（論理式の集合 Γ に置換を適用してσ Γ = { σA : A ∈ Γ} とすることもできます。）タルスキ型の帰結関係^{[ 1 ]}は、${\displaystyle \vdash }$数式と数式の間に、

すべての式A、B、および式の集合 Γ、Δ に対して。次のような帰結関係

すべての置換σについて、構造的と呼ばれる。（ここでおよび以下で使用される「構造的」という用語は、シーケント計算における構造規則の概念とは無関係であることに注意。）構造的帰結関係は命題論理と呼ばれる。論理式Aは論理の定理である。${\displaystyle \vdash }$もし${\displaystyle \varnothing \vdash A}$。

例えば、超直観主義論理Lをその標準的な帰結関係と同一視する。$\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 \sigma A_{1},\dots ,\sigma A_{n}/\sigma B}$

置換σの場合。規則Γ/ Bは導出可能であり、${\displaystyle \vdash }$、 もし${\displaystyle \Gamma \vdash B}$規則のすべてのインスタンスについて、σΓからのすべての式が定理である場合にσBが定理である場合、それは許容される。^{[ 3 ]}言い換えれば、規則が論理に追加されても新しい定理を導かない場合、その規則は許容される。^{[ 4 ]}また、次のように書く。${\displaystyle \Gamma \mathrel {|\!\!\!\sim } B}$Γ/ Bが許容される場合。（注意：${\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}$（それ自体が構造的な帰結関係である。）

導出可能な規則はすべて許容可能だが、一般にその逆は成り立たない。論理は、許容可能な規則がすべて導出可能である場合、すなわち、構造的に完全である。${\displaystyle {\vdash }={\,|\!\!\!\sim }}$[ ^{5 ]​}

適切な論理結合子を持つ論理体系（超直観主義論理や様相論理など）では、規則${\displaystyle A_{1},\dots ,A_{n}/B}$と同等${\displaystyle A_{1}\land \dots \land A_{n}/B}$許容性および導出可能性に関して。したがって、単項規則A / Bのみを扱うのが慣例です。

• 古典命題論理( CPC ) は構造的に完全である。^{[ 6 ]}実際、A / Bは非導出規則であると仮定し、v ( A ) = 1、v ( B ) = 0となるような割り当てvを固定する。すべての変数pに対して、σp =となるような置換σを定義する。${\displaystyle \top }$v ( p ) = 1 の場合、σp =${\displaystyle \bot }$v ( p ) = 0の場合、 σAは定理ですが、σB は定理ではありません（実際には、¬σBは定理です）。したがって、規則A / Bも許容されません。（この議論は、すべての要素がLの言語で名前を持つ論理行列に関して完全な任意の多値論理Lにも適用されます。）
• クライゼル＝パトナムの法則（ハロップの法則、または前提の独立性の法則とも呼ばれる）

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

直観主義命題論理（IPC ）では許容される。実際、あらゆる超直観主義論理で許容される。^{[ 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、K4、S4、GLなどの多くの様相論理で許容されます（様相論理の名前については、この表を参照してください）。S4では導出可能ですが、K、D、K4、GLでは導出できません。

• ルール

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

通常の論理では許容される${\displaystyle L\supseteq S4.3}$^{[ 8 ]} GLとS 4.1では導出可能ですが、 K、D、K 4、S 4、S 5では導出できません。

• レープの法則

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

は基本様相論理Kでは許容される（ただし導出はできない）が、 GLでは導出可能である。しかし、LR はK 4では許容されない。特に、論理Lで許容される規則がその拡張で許容されるとは限りません。

• ゲーデル・ダメット論理（LC）と様相論理Grz.3は構造的に完全である。^{[ 9 ]}積ファジィ論理も構造的に完全である。^{[ 10 ]}

与えられた論理の許容規則に関する基本的な問題は、すべての許容規則の集合が決定可能かどうかである。論理自体（つまり、その定理の集合）が決定可能であっても、この問題は自明ではないことに注意されたい。規則A / Bの許容性の定義には、すべての命題置換に対する無制限の全称量化子が含まれる。したがって、先験的に、決定可能な論理における規則の許容性は、$\displaystyle \Pi _{1}^{0}}$（つまり、その補集合は再帰的に列挙可能である）。例えば、双様論理K _uおよびK 4 _u （普遍様相を持つKまたはK 4の拡張）における許容性は決定不能であることが知られている。^{[ 11 ]}驚くべきことに、基本様相論理Kにおける許容性の決定可能性は、主要な未解決問題である。

それにもかかわらず、規則の許容性は多くの様相論理および超直観主義論理において決定可能であることが知られている。基本的な推移的様相論理における許容規則の最初の決定手続きは、規則の縮約形を用いてRybakovによって構築された。^{[ 12 ]}変数p0 , ..., pk_の様相規則は、次の形式を持つ場合に縮約形と呼ばれる_。

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

それぞれ${\displaystyle \neg _{i,j}^{u}}$空白または否定${\displaystyle \neg }$各規則rに対して、A 内のすべての部分式に拡張変数を導入し、結果を完全な選言標準形で表現することにより、任意の論理が r を許容（または導出）する場合に限り s を許容（または導出）するような、簡約規則s（rの簡約形と呼ばれる）を効果的に構築できます。したがって、簡約規則の許容性に関する決定アルゴリズムを構築すれば十分です。

させて${\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\}}$その結合子の。集合の任意の部分集合Wに対して${\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 ]}

定理。規則${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$K 4では、集合が存在する場合に限り許容されない。${\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. Wの任意の部分集合Dに対して、要素が存在する${\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に対して成り立つ。

同様の基準は、 S 4、GL、およびGrz の論理にも見られます。^{[ 14 ]}さらに、直観主義論理における許容性は、ゲーデル–マッキンゼー–タルスキ変換を使用してGrzにおける許容性に還元できます。^{[ 15 ]}

${\displaystyle A\,|\!\!\!\sim _{IPC}B}$かつその場合に限り${\displaystyle T(A)\,|\!\!\!\sim _{Grz}T(B).}$

Rybakov (1997) は、許容性の決定可能性を示すためのより洗練された手法を開発しました。これは、 S 4.1、S 4.2、S 4.3、KC、T _k (および上述のIPC、 K 4、S 4、GL、Grzの論理) を含む、推移的(つまりK 4 またはIPCを拡張する) 様相論理および超直観主義論理の堅牢な (無限) クラスに適用されます。^{[ 16 ]}

決定可能であるにもかかわらず、許容性問題は、単純な論理体系であっても、比較的高い計算複雑性を持つ。基本的な推移的論理体系であるIPC、K 4、S 4、GL、Grzにおける規則の許容性はcoNEXP完全である。^{[ 17 ]}これは、これらの論理体系における導出可能性問題 (規則または式の場合) とは対照的である。導出可能性問題はPSPACE完全である。^{[ 18 ]}

命題論理における許容性は、様相代数またはヘイティング代数の等式理論における統一と密接に関連している。この関連性はギラールディ（1999、2000）によって発展させられた。論理的設定において、論理言語Lの式Aの統一子（略してL統一子）は、 σAがLの定理となるような置換σである。（この概念を用いると、 Lにおける規則A / Bの許容性を「AのすべてのL統一子はBのL統一子である」と言い換えることができる。）L統一子σは、ある置換υが存在して、 L統一子τよりも一般性が低い、つまりσ ≤ τと表される。

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

すべての変数pについて。式Aの L -統一子の完全な集合は、 AのL - 統一子の集合Sであり、 AのすべてのL - 統一子はSのいずれかの統一子よりも一般性が低い。Aの最も一般的な統一子( MGU )は、 { σ } がAの完全な統一子の集合であるような統一子σである。したがって、S がAの完全な統一子の集合である場合、規則A / BがL - 許容可能であるのは、 SのすべてのσがBのL - 統一子である場合のみである。したがって、性質の良い完全な統一子の集合を見つけることができれば、許容可能な規則を特徴付けることができる。

最も一般的な統一子を持つ重要な論理式のクラスは射影論理式です。これらは、Aの統一子σが存在して、

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

すべての式Bについて。σ は A の MGU であることに注意してください。有限モデル特性を持つ推移的様相論理および超直観主義論理では、射影式を意味論的に、有限Lモデルの集合が拡張特性を持つものとして特徴付けることができます。^{[ 19 ]} Mが、クラスターが単一であるルートrを持つ有限 Kripke Lモデルであり、式A がrを除くMのすべての点で成り立つ場合、 rの変数の評価を変更して、A がrでも真になるようにすることができます。さらに、証明は、与えられた射影式Aの MGU の明示的な構成を提供します。

基本的な推移的論理IPC、K 4、S 4、GL、Grz（およびより一般的には、有限フレームの集合が別の種類の拡張特性を満たす有限モデル特性を持つ任意の推移的論理）では、任意の式Aに対して、その射影近似Π( A ) を効果的に構成できます。^{[ 20 ]}次のような射影式の有限集合。

1. ${\displaystyle P\vdash _{L}A}$すべての${\displaystyle P\in \Pi (A),}$
2. Aのすべての統一子は、 Π( A )の式の統一子である。

したがって、Π( A )の要素のMGUの集合は、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を論理体系とする。L許容規則の集合Rは、すべての許容規則 Γ/ Bが置換、合成、弱化を用いてRとLの導出可能な規則から導出できる場合、許容規則の基底^{[ 22 ]}と呼ばれる。言い換えれば、Rが基底であるのは、以下の条件を満たす場合のみである。${\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}}$は、以下を含む最小の構造的帰結関係です。$\displaystyle \vdash _{L}}$そしてR。​

決定可能な論理の許容規則の決定可能性は、再帰的（または再帰的に列挙可能）基底の存在と同等であることに注意してください。一方では、許容性が決定可能であれば、すべての許容規則の集合は再帰的基底です。他方では、許容規則の集合は常に共再帰的に列挙可能であり、さらに再帰的に列挙可能な基底があれば、許容規則の集合も再帰的に列挙可能になります。したがって、それは決定可能です。（言い換えれば、次のアルゴリズムによってA / Bの許容性を決定できます。A を統一するがB を統一しない置換σを探すための 1 つと、 RからA / Bを導出するための 1 つの、2 つの総当たり探索を並行して開始します。$\displaystyle \vdash _{L}}$（いずれか1つの探索で答えが見つかるはずです。）決定可能性とは別に、許容規則の明示的な基底は、証明の複雑さなどのいくつかのアプリケーションで役立ちます。^{[ 23 ]}

与えられた論理体系に対して、それが許容規則の再帰的基底または有限基底を持つかどうかを問い、明示的な基底を与えることができる。論理体系が有限基底を持たない場合でも、独立した基底、すなわち、 Rの真部分集合が基底とならないような基底Rを持つことができる。

一般的に、望ましい性質を持つ基底の存在についてはほとんど何も言えません。たとえば、表形式論理は一般的に振る舞いが良く、常に有限に公理化可能ですが、有限または独立した規則基底を持たない表形式様相論理が存在します。^{[ 24 ]}有限基底は比較的まれです。基本的な推移的論理であるIPC、K4、S4、GL、Grzでさえ、独立した基底は持っているものの、許容規則の有限基底を持っていません。^{[ 25 ] [ 26 ]}

規則Γ/ Bは様相的または直観主義的クリプキフレームにおいて有効である。${\displaystyle F=\langle W,R\rangle }$すべての評価について以下が真である場合${\displaystyle \Vdash }$Fで：

すべての場合${\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の反射的タイト前任者、Wのすべてのyに対してt R yであるのはt = yの場合のみ、またはXのあるxに対してx = yまたはx R yである場合。
• Xの非反射的タイト前任者とは、Wのすべてのyに対してt R yであるのは、 Xのあるxに対してx = yまたは x R yである場合に限る。

フレームFが反射的（非反射的）タイトな先行要素を持つとは、Wの任意の有限部分集合Xに対して、 W内にXの反射的（非反射的）タイトな先行要素が存在する場合をいう。

我々には以下がある：^{[ 31 ]}

• IPCにおいて規則が許容されるのは、それが反射的に厳密な先行規則を持つすべての直観主義的枠組みにおいて有効である場合に限る。
• 規則が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 は、遺伝的に構造的に完全である。遺伝的に構造的に完全な超直観主義論理と推移的様相論理の完全な記述は、それぞれ Citkin と Rybakov によって与えられた。すなわち、超直観主義論理は、5 つの Kripke フレーム^{[ 9 ]}のいずれにおいても有効でない場合のみ、遺伝的に構造的に完全である。

同様に、 K 4の拡張は、特定の 20 のクリプキ フレーム (上記の 5 つの直観主義フレームを含む) のいずれにおいても有効でない場合のみ、遺伝的に構造的に完全である。^{[ 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に分けられる。規則は、各iについてσs _i = s _iとなるAのすべてのL - 単一化子σがBの単一化子でもある場合にL - 許容可能である。許容規則に関する基本的な決定可能性の結果は、パラメータを持つ規則にも適用される。^{[ 34 ]}  

多重結論ルールは、2 つの有限な式の集合 (Γ,Δ) のペアであり、次のように記述されます。

$\displaystyle {\frac {A_{1},\dots ,A_{n}}{B_{1},\dots ,B_{m}}}\qquad {\text{または}}\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 }$。

• 新しい定数名と関数名による拡張
• 保守的な拡張

• W. Blok、D. Pigozzi、「代数化可能な論理」、アメリカ数学会紀要77（1989）、第396号、1989年。
• A. チャグロフ、M. ザハリャシェフ著『様相論理』、オックスフォード論理ガイド第35巻、オックスフォード大学出版局、1997年。ISBN 0-19-853779-4
• P. Cintula、G. Metcalfe、「ファジィ論理における構造的完全性」、Notre Dame Journal of Formal Logic 50 (2009)、第 2号、pp.  153–182。doi : 10.1215/00294527-2009-004
• AI Citkin、「構造的に完全な超直観主義論理について」  、ソビエト数学 - Doklady、第19巻（1978年）、 816 ～ 819ページ。
• S. Ghilardi、「直観主義論理における統一」、Journal of Symbolic Logic 64 (1999)、第2号、pp.  859–880。Project Euclid JSTOR
• S. Ghilardi、 「モーダル方程式の最適解法」、Annals of Pure and Applied Logic 102 (2000)、第3号、pp.  183–198。doi : 10.1016/S0168-0072(99)00032-9
• R. Iemhoff、「直観主義命題論理の許容規則について」、Journal of Symbolic Logic 66 (2001)、第1号、pp.  281–294。Project Euclid JSTOR
• R. Iemhoff、「中間論理とヴィッサーの規則」、ノートルダム形式論理ジャーナル46（2005）、第1号、 65-81ページ。doi ：10.1305 /ndjfl/1107220674
• R. Iemhoff、「中間論理の規則について」、 Archive for Mathematical Logic、45 (2006)、第5号、pp.  581–599。doi : 10.1007/s00153-006-0320-8
• E. Jeřábek、「様相論理の許容規則」、Journal of Logic and Computation 15 (2005)、第4号、pp.  411–431。doi : 10.1093/logcom/ exi029
• E. Jeřábek、「許容規則の複雑性」、Archive for Mathematical Logic 46 (2007)、第2号、 73–92頁。doi : 10.1007 /s00153-006-0028-9
• E. Jeřábek、「許容規則の独立基底」、Logic Journal of the IGPL 16 (2008)、第3号、pp. 249–267。doi  : 10.1093 /jigpal/jzn004
• M. Kracht、「様相論理の帰結関係」、『様相論理ハ​​ンドブック』（P. Blackburn、J. van Benthem、F. Wolter 編）、論理と実践的推論研究 第3巻、Elsevier、2007年、 492-545頁。ISBN 978-0-444-51690-9
• P. Lorenzen、Einführung in die oper Logik und Mathematik、Grundlehren der mathematischen Wissenschaften vol. 78、シュプリンガー – フェルラーク、1955 年。
• G. Mints および A. Kojevnikov、「直観主義的なフレーゲ システムは多項式的に等価である」、Zapiski Nauchnyh Seminarov POMI 316 (2004)、129 ～ 146 ページ 。gzip 圧縮された PS
• T. Prucnal、「メドベージェフ命題論理の構造的完全性」、数理論理学報告6（1976）、pp.  103–105。
• T. Prucnal、「ハーヴェイ・フリードマンの2つの問題について」、Studia Logica 38 (1979)、第3号、pp. 247–262。doi  : 10.1007 /BF00405383
• P. ロジエール、直感的計算命題の許容範囲、Ph.D.論文、パリ第 7 大学、1992 年。PDF
• VV Rybakov、「論理的推論規則の許容性」、論理学と数学の基礎に関する研究、第136巻、Elsevier、1997年。ISBN 0-444-89505-1
• F. Wolter、M. Zakharyaschev、「様相論理と記述論理における統一問題と許容性問題の決定不能性」、ACM Transactions on Computational Logic 9 (2008)、第4号、論文番号25。doi : 10.1145/1380572.1380574 PDF