中間ロジック

数理論理学において、超直観主義論理は直観主義論理を拡張した命題論理である。 古典論理は最も一貫性のある超直観主義論理であるため、一貫性のある超直観主義論理は中間論理と呼ばれる（その論理は直観主義論理と古典論理の中間である）。^[1]

超直観論理とは、次の特性を満たす 変数p _iの可算集合内の命題式の集合Lです。

1.直観主義論理のすべての公理はLに属する。

2. FとGが式であり、FとF → G が両方ともLに属する場合、GもLに属する（モーダスポネンスによる閉包）。

3. F ( p ₁ , p ₂ , ..., p _n ) がLの式であり、G ₁ , G ₂ , ..., G _nが任意の式である場合、F ( G ₁ , G ₂ , ..., G _n ) はLに属します(置換による閉包)。

このような論理は、さらに

4. L はすべての式の集合ではありません。

異なる中間論理の連続体が存在し、そのような論理の多くに選言特性(DP) が見られます。超直観主義論理または中間論理は、直観主義論理を底辺、矛盾論理 (超直観主義論理の場合) または古典論理 (中間論理の場合) を頂点とする完全な格子を形成します。古典論理は、超直観主義論理の格子における唯一のコアトムです。中間論理の格子にも、 SmLという固有のコアトムがあります^[要出典]。

中間論理を研究するためのツールは、クリプキ意味論などの直観主義論理に使用されるものと似ています。たとえば、ゲーデル・ダメット論理は、全順序の観点から単純な意味的特徴付けを持っています。特定の中間論理は、意味的記述によって与えられる場合があります。

他のものは、1つ以上の公理を追加することで与えられることが多い。

• 直観主義論理（通常は直観主義命題計算IPCと表記されるが、Int、IL、Hとも表記される）

例:

• 古典論理（CPC、Cl、CL）：

= IPC + ¬¬ p → p (二重否定除去、DNE)

= IPC + (ε p → p ) → p (ミラビリス)

= IPC + p ∨ ¬ p (排中律、PEM)

上記の一般化された変種（ただし、直観主義論理上の原理は実際には同等）は、それぞれ、

= IPC + (¬ p → ¬ q ) → ( q → p )（逆対置原理）

= IPC + (( p → q ) → p ) → p (ピアスの原理PP、Consequentia mirabilis と比較)

= IPC + ( q → p ) → ((したq → p ) → p ) (Consequentia mirabilis を一般化する別のスキーマ)

= IPC + p ∨ ( p → q ) （PEMから爆発の原理を経て）

• スメタニッチの論理（SmL）：

= IPC + (¬ q → p ) → ((( p → q ) → p ) → p ) (条件付きPP)

• ゲーデル-ダメット論理(ダメット1959) ( LCまたはG、下記の拡張を参照):

= IPC + ( p → q ) ∨ ( q → p ) (ダーク・ジェントリーの原理、DGP、または線形性)

= IPC + ( p → ( q ∨ r )) → (( p → q ) ∨ ( p → r )) (前提IPの独立性の一形態)

= IPC + (( p ∧ q ) → r ) → (( p → r ) ∨ ( q → r )) (一般化された第4ド・モルガンの法則)

• 制限された深さ2（BD2、以下の一般化を参照。p∨ （p → q _）と比較してください）：

= IPC + p ∨ ( p → ( q ∨ ¬ q ))

• ヤンコフの論理（1968）^[2]またはド・モルガンの論理（KC）：

= IPC + ¬¬ p ∨ ¬ p (弱いPEM、別名WPEM)

= IPC + ( p → q ) ∨ (¬ p → ¬ q ) (弱いDGP)

= IPC + ( p → ( q ∨ ¬ r )) → (( p → q ) ∨ ( p → ¬ r )) (IP の形式の否定を伴う変形)

= IPC + ¬( p ∧ q ) → (¬ q ∨ ¬ p ) (第4ド・モルガンの法則)

• スコットの論理（SL）：

= IPC + ((¬¬ p → p ) → ( p ∨ ¬ p )) → (¬¬ p ∨ ¬ p ) (条件付きWPEM)

• クライゼル–パトナム論理 ( KP ):

= IPC + (¬ p → ( q ∨ r )) → ((¬ p → q ) ∨ (¬ p → r )) (IP の形式の否定を伴う他の変形)

このリストは、大部分において、順序付けされていません。たとえば、LC はSmLのすべての定理を証明できないことが知られていますが、その強さはBD ₂と直接比較できるものではありません。同様に、たとえば、KP はSLと比べられません。各ロジックの等式のリストも、決して網羅的ではありません。たとえば、WPEM やド・モルガンの法則と同様に、結合を使用する DGP のいくつかの形式を表現できます。

WPEMをさらに弱めた(¬¬ p ∨ ¬ p ) ∨ (¬¬ p → p )でさえ、IPCの定理ではありません。

また、直観主義論理のすべてを当然のこととして考えると、等式は爆発に大きく依存していることも注目に値するかもしれません。たとえば、単なる極小論理では、原理として PEM はすでに Consequentia mirabilis と同等ですが、より強い DNE や PP を意味するわけではなく、DGP と比較することもできません。

進行中:

• 制限された深さの論理（BD _n）：

IPC + p _n ∨ ( p _n → ( p _{n −1} ∨ ( p _{n −1} → ... → ( p ₂ ∨ ( p ₂ → ( p ₁ ∨ æ p ₁ )))...)))

• ゲーデルの n値論理（G _n）:

LC + BD _{n −1}

= LC + BC _{n −1}

• 有界基数の論理（BC _n）：

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to p_{i}{\bigr )}}$

• 上限幅（BTW _n）のロジック：

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to \neg \neg p_{i}{\bigr )}}$

• 制限された幅の論理、制限された反連鎖の論理としても知られる、小野（1972）（BW _n、BA _n）：

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j\neq i}p_{j}\to p_{i}{\bigr )}}$

• 有界分岐の論理、Gabbay & de Jongh (1969, 1974) ( T _n、BB _n ):

${\displaystyle \textstyle \mathbf {IPC} +\bigwedge _{i=0}^{n}{\bigl (}{\bigl (}p_{i}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{i=0}^{n}p_{i}}$

さらに：

• 実現可能性の論理
• メドヴェージェフの有限問題論理（LM、ML）: ^{[3] [4] [5]}有限集合X （「頂点のないブール超立方体」）の形式すべてのフレームの論理として意味的に定義され、再帰的に公理化可能であることは知られていない${\displaystyle \langle {\mathcal {P}}(X)\setminus \{X\},\subseteq \rangle }$
• ...

命題論理SLとKPには、選言特性 DP があります。クリーネ実現可能性論理と強いメドベージェフ論理にもこれがあります。格子上に DP を持つ唯一の最大論理はありません。一貫性のある理論が WPEM を検証しても、PEM を仮定したときに独立したステートメントがまだある場合、DP を持つことはできないことに注意してください。

ヘイティング代数 Hが与えられた場合、 Hで有効な命題式の集合は中間論理です。逆に、中間論理が与えられた場合、そのリンデンバウム-タルスキー代数 を構築することができ、それはヘイティング代数になります。

直観主義クリプキフレーム Fは半順序集合であり、クリプキモデルMは、 がFの上部分集合となるような付値を持つクリプキフレームです。 Fで有効な命題式の集合は中間論理です。中間論理Lが与えられれば、 Mの論理がLとなるようなクリプキモデルM を構築することができます(この構築は標準モデルと呼ばれます)。この特性を持つクリプキフレームは存在しないかもしれませんが、一般的なフレームは必ず存在します。 ${\displaystyle \{x\mid M,x\Vdash p\}}$

A を命題式とします。Aのゲーデル-タルスキ変換は次のように再帰的に定義されます。

• ${\displaystyle T(p_{n})=\Box p_{n}}$
• ${\displaystyle T(\neg A)=\Box \neg T(A)}$
• ${\displaystyle T(A\land B)=T(A)\land T(B)}$
• ${\displaystyle T(A\vee B)=T(A)\vee T(B)}$
• ${\displaystyle T(A\to B)=\Box (T(A)\to T(B))}$

M がS4 を拡張する様相論理である場合、ρ M = { A | T ( A ) ∈ M }は超直観論理であり、M はρ Mの様相伴者と呼ばれる。特に:

• IPC = ρS4
• KC = ρS4.2 である。
• LC = ρS4.3
• CPC = ρS5

すべての中間論理Lに対して、 L  = ρ Mとなるような様相論理Mが多数存在します。

• 論理システムの一覧

• チャグロフ、アレクサンダー、ザカリャシェフ、マイケル (1997)。様相論理。オックスフォード:クラレンドン プレス。p. 605。ISBN 9780198537793。

• Medvedev, Yu T. (1962). 「有限問題」(PDF) .ソビエト数学(ロシア語). 3 (1): 227–230. doi :10.2307/2272084. JSTOR  2272084. Elliott Mendelson による XXXVIII 356(20) の英語翻訳。
• Medvedev, Yu T. (1963). 「有限問題による論理式の解釈と可読性理論との関係」( PDF)。Soviet Mathematics (ロシア語)。4 ( 1): 180–183。doi :10.2307/2272084。JSTOR  2272084。Sue Ann Walker による XXXVIII 356 ( 21) の英語翻訳。
• Medvedev, Yu T. (1966). 「[有限問題による論理式の解釈]」(PDF) .ソビエト数学(ロシア語). 7 (4): 857–860. doi :10.2307/2272084. JSTOR  2272084. Sue Ann Walker による XXXVIII 356(22) の英語翻訳

• テルウィン、セバスティアン A. (2006)。 「構成的論理とメドベージェフ格子」。ノートルダム形式論理ジャーナル。47 (1): 73–82。土井：10.1305/ndjfl/1143468312。

• 梅沢俊夫 (1959 年 6 月). 「直観主義的述語論理と古典的述語論理の中間の論理について」.記号論理学ジャーナル. 24 (2): 141–153. doi :10.2307/2964756. JSTOR  2964756. S2CID  13357205.

• 「中間論理」、数学百科事典、EMS Press、2001 [1994]