直観主義論理

直観主義論理の論理式の構文は古典命題論理や古典述語論理と類似である。しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため ${\displaystyle \{\to ,\bot \}}$ , ${\displaystyle \{\wedge ,\neg \}}$ , ${\displaystyle \{\vee ,\neg \}}$  などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に${\displaystyle \to ,\wedge ,\vee ,\bot }$  を基本的な結合子として採用する。ここで ${\displaystyle \neg A}$  は ${\displaystyle A\to \bot }$  の省略形として扱う。直観主義述語論理ではこれに量化記号 ${\displaystyle \exists ,\forall }$  を加える。

多くの古典論理の恒真式は直観主義的には証明できない。排中律 ${\displaystyle p\vee \neg p}$  だけでなくパースの法則 ${\displaystyle ((p\to q)\to p)\to p}$  や二重否定除去 ${\displaystyle \neg \neg p\to p}$  などがその例である。古典論理において二重否定導入 ${\displaystyle p\to \neg \neg p}$  と二重否定除去 はともに定理である。直観主義論理においては前者のみが定理である。すなわち二重否定を導入することはできるが、除去することはできない。ただし三重否定除去 ${\displaystyle \neg \neg \neg p\to \neg p}$  は定理である。排中律 ${\displaystyle p\vee \neg p}$  の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。

多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。

ゲンツェンは彼の体系LK（古典論理のシークエント計算）の簡単な制限として直観主義論理の健全かつ完全な体系が得られることを見つけた。彼はこの体系をLJと呼んだ。LKにおいて任意個の論理式がシークエントの結論（右側）に来ることを許すが、LJにおいては高々ひとつの論理式だけを許す。この結果として例えば含意右の適用において直観主義的に許容できない推論が禁じられることから、直観主義論理の体系が得られるのである。（右辺が複数であることを許すと含意右を用いて α→α,⊥ から →α,￢α が得られ、排中律が導かれる。右辺を制限した結果として含意右が制限されて直観主義論理の体系が得られる。）

LKを制限して得られる直観主義論理の体系で結論が複数であることを許容するものもある。LJ'^[1]はその例である。

直観主義論理は次のようにヒルベルト流の計算を用いても定義できる。これは古典命題論理の公理化（Propositional calculus#Alternative calculus）に類似である。

命題論理では、推論規則としてモーダスポネンス

• MP: ${\displaystyle \phi }$  および ${\displaystyle \phi \to \psi }$  から ${\displaystyle \psi }$  を導く

を取り、公理図式として次のものを取る：

• THEN-1: ${\displaystyle \phi \to (\chi \to \phi )}$ 
• THEN-2: ${\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))}$ 
• AND-1: ${\displaystyle \phi \land \chi \to \phi }$ 
• AND-2: ${\displaystyle \phi \land \chi \to \chi }$ 
• AND-3: ${\displaystyle \phi \to (\chi \to (\phi \land \chi ))}$ 
• OR-1: ${\displaystyle \phi \to \phi \lor \chi }$ 
• OR-2: ${\displaystyle \chi \to \phi \lor \chi }$ 
• OR-3: ${\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))}$ 
• FALSE: ${\displaystyle \bot \to \phi }$ 

一階述語論理の体系を作るには次の推論規則を加える：

• ${\displaystyle \forall }$ -GEN: ${\displaystyle \psi \to \phi }$  から ${\displaystyle \psi \to (\forall x\ \phi )}$  を導く；ただし固有変数条件「${\displaystyle x}$  は ${\displaystyle \psi }$  に自由に現れない」を満たす
• ${\displaystyle \exists }$ -GEN: ${\displaystyle \phi \to \psi }$  から ${\displaystyle (\exists x\ \phi )\to \psi }$  を導く；ただし固有変数条件「${\displaystyle x}$  は ${\displaystyle \psi }$  に自由に現れない」を満たす

また次のものを公理図式に加える：

• PRED-1: ${\displaystyle (\forall x\ \phi (x))\to \phi (t)}$  ただし項 t は ${\displaystyle \phi }$  の中の x への代入について自由である (つまり t の中の変数記号は ${\displaystyle \phi (t)}$  の中で束縛されていない)
• PRED-2: ${\displaystyle \phi (t)\to (\exists x\ \phi (x))}$  ただしPRED-1と同様の条件を満たす

もし否定を表す結合子 ${\displaystyle \lnot }$  を ${\displaystyle \phi \to \bot }$  なる省略形の代わりに導入したいならば、次を公理に加えれば十分である：

• NOT-1': ${\displaystyle (\phi \to \bot )\to \lnot \phi }$ 
• NOT-2': ${\displaystyle \lnot \phi \to (\phi \to \bot )}$ 

否定を導入した代わりに偽を表す命題定数 ${\displaystyle \bot }$  を落としたいならば次のようにする。まず FALSE, NOT-1', NOT-2' を次の公理に置き換える：

• NOT-1: ${\displaystyle (\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )}$ 
• NOT-2: ${\displaystyle \phi \to (\lnot \phi \to \chi )}$ 

NOT-1の代替としては ${\displaystyle (\phi \to \lnot \chi )\to (\chi \to \lnot \phi )}$  または ${\displaystyle (\phi \to \lnot \phi )\to \lnot \phi }$  などがある。

同値を表す結合子 ${\displaystyle \leftrightarrow }$  は ${\displaystyle \phi \leftrightarrow \chi }$  standing for ${\displaystyle (\phi \to \chi )\land (\chi \to \phi )}$  の省略形として導入できる。代わりに次の公理を追加してもよい：

• IFF-1: ${\displaystyle (\phi \leftrightarrow \chi )\to (\phi \to \chi )}$ 
• IFF-2: ${\displaystyle (\phi \leftrightarrow \chi )\to (\chi \to \phi )}$ 
• IFF-3: ${\displaystyle (\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))}$ 

IFF-1とIFF-2は一つの公理 ${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$  に結合できる。

古典論理の体系は次のどれかを公理に追加することによって得られる：

• ${\displaystyle \phi \lor \lnot \phi }$  （排中律。これは ${\displaystyle (\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}$  とも定式化できる。）
• ${\displaystyle \lnot \lnot \phi \to \phi }$  （二重否定除去）
• ${\displaystyle ((\phi \to \chi )\to \phi )\to \phi }$  （パースの法則）

一般に、古典論理の恒真式で二元クリプキ・フレーム ${\displaystyle \circ {\longrightarrow }\circ }$  で妥当でない公理を追加したもの（言い換えればSmetanich論理に含まれないもの）を考えれば、これは古典論理に等しい。Smetanich論理は古典論理よりも弱く直観主義論理より強い論理の中で極大なものだからである。

別の関係性としてはゲーデル＝ゲンツェン変換によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。またグリベンコの定理によれば、命題論理式が古典論理で証明可能であることと、それを二重否定したものが直観主義論理で証明可能であることとは同値である。したがって直観主義論理は古典論理を構成的意味論の観点から拡大したものと見做すことができる。

1932年にクルト・ゲーデルは古典論理と直観主義論理の間にあるゲーデル論理の体系を定義した。これは中間論理として知られる。

古典命題論理において、論理積、論理和または実質含意を基本的なものとすれば、他は否定を用いてウカシェヴィッチの命題論理のようにして定義できる。またこれら4つをパースの矢印（NOR）やシェファーの棒（NAND）のようなただひとつの論理結合子を用いて定義することもできる。同様に、古典一階述語論理において、一方の量化子は他方と否定を用いて定義できる。

これらは全ての結合子はブール関数であるという二値原理からの基本的な帰結である。二値原理は直観主義論理においては成り立たない。ただ無矛盾律だけが成り立つ。結果として、いかなる結合子も不要ではなく、上に述べたどの公理も必要であることが分かる。古典論理において成立する同値性は、直観主義論理においては、幾つかは成り立つけれども、多くは一方の含意だけが成り立つ。次のようなものがある：

論理積と論理和：

• ${\displaystyle (\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )}$ 
• ${\displaystyle (\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )}$ 
• ${\displaystyle (\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )}$ 
• ${\displaystyle (\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )}$ 

論理積と含意：

• ${\displaystyle (\phi \wedge \psi )\to \neg (\phi \to \neg \psi )}$ 
• ${\displaystyle (\phi \to \psi )\to \neg (\phi \wedge \neg \psi )}$ 
• ${\displaystyle (\phi \wedge \neg \psi )\to \neg (\phi \to \psi )}$ 
• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )}$ 

論理和と含意：

• ${\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}$ 
• ${\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}$ 

全称量化と存在量化：

• ${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$ 
• ${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$ 
• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$ 
• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$ 

すると、例えば、 "a or b" は "if not a, then b" よりも強い主張となる。これは古典論理において同値であることと対照的である。他方で "not (a or b)" と "not a, and also not b" は同値となる。

同値を結合子のリストに入れるならば、いくつかの結合子は他から定義できる：

• ${\displaystyle (\phi \leftrightarrow \psi )\leftrightarrow ((\phi \to \psi )\land (\psi \to \phi ))}$ 
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}$ 
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}$ 
• ${\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}$ 
• ${\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}$ 

とりわけ ${\displaystyle \{\vee ,\leftrightarrow \bot \}}$  と ${\displaystyle \{\vee ,\leftrightarrow \neg \}}$  は直観主義的結合子の完全な基底となる。

直観主義論理の意味論は古典論理のそれよりも複雑である。直観主義論理のモデル論はハイティング代数やクリプキ意味論として与えられている。最近ではタルスキ流のモデル論の完全性がBob Constableによって証明せられた。ただしこの完全性は通常の意味のそれとは異なる。

古典論理において、我々はしばしば論理式の取る真理値について議論する。この値は普通はブール代数の元から選ぶ。ブール代数の交わりと結びは論理結合子の ${\displaystyle \wedge }$  と ${\displaystyle \vee }$  に同一視される。そして ${\displaystyle A\wedge B}$  の真理値は ${\displaystyle A}$  と ${\displaystyle B}$  の真理値のブール代数における交わりとする。このとき論理式が古典論理において妥当であることと、任意のブール代数とその上で値を取る真理値割り当てに対して論理式の真理値が ${\displaystyle \top }$  であることとが同値となる。

直観主義論理においても同様の完全性定理が成立するが、論理式の真理値はブール代数の代わりにハイティング代数の元を用いる。ブール代数はハイティング代数の特別な場合である。このとき論理式が直観主義論理で妥当であることと、任意のハイティング代数とその上で値を取る真理値割り当てに対して論理式の真理値が ${\displaystyle \top }$  であることは同値である。

論理式が妥当であることを確かめる為には、ひとつのハイティング代数の上で調べれば十分であることが証明できる。そのハイティング代数は数直線 ${\displaystyle \mathbb {R} }$  の開部分集合からなるハイティング代数である。^[2] この代数系において、${\displaystyle \wedge }$  と ${\displaystyle \vee }$  は集合の交わりと結びである。また ${\displaystyle A\to B}$  は ${\displaystyle \mathrm {int} (A^{c}\cup B)}$  すなわち ${\displaystyle A}$  の補集合と ${\displaystyle B}$  との和集合の内部である。（これは古典論理における含意の演算の結果を開集合になるように調整したものである。様相論理の観点から見るとこれは必然性を外側に付けているのと同じことになる。）${\displaystyle \bot }$  は空集合 ${\displaystyle \varnothing }$  であり、${\displaystyle \top }$  は全体集合 ${\displaystyle \mathbb {R} }$  である。否定 ${\displaystyle \neg A}$  は ${\displaystyle A\to \bot }$  と定義されるが、これは ${\displaystyle A}$  の補集合の開核すなわち外部と一致する。この対応付けによって直観主義的に妥当な論理式はちょうど空間全体が割り当てられるものと一致する。^[2]

例えば矛盾律 ${\displaystyle \neg (A\wedge \neg A)}$  は妥当である。なぜなら開集合 ${\displaystyle X}$  を ${\displaystyle A}$  の付値としてどのように選んでも ${\displaystyle \neg (A\wedge \neg A)}$  の値は次のように直線全体となるからである：

${\displaystyle \mathrm {val} (\neg (A\wedge \neg A))=\mathrm {int} ((X\wedge \mathrm {int} (X^{c}))^{c})}$ 

位相空間論によれば ${\displaystyle \mathrm {int} (X^{c})}$  は ${\displaystyle X^{c}}$  の部分集合であり、${\displaystyle X}$  との共通部分は空であるから、

${\displaystyle \mathrm {int} (\varnothing ^{c})=\mathrm {int} (\mathbb {R} )=\mathbb {R} }$ 

したがってこの論理式の付値は真であり、妥当であることが従う。

しかし排中律 ${\displaystyle A\vee \neg A}$  は非妥当である。それには ${\displaystyle A}$  に ${\displaystyle (0,\infty )}$  を���り当てるとよい。すると ${\displaystyle \neg A}$  の付値は ${\displaystyle (-\infty ,0]}$  の内部、すなわち ${\displaystyle (-\infty ,0)}$  であり、目的の論理式の付値は ${\displaystyle (0,\infty )}$  および ${\displaystyle (-\infty ,0)}$  の和集合、すなわち ${\displaystyle \mathbb {R} \setminus \{0\}}$  となる。これは空間全体に一致しない。

数直線からハイティング代数を作る上のやり方は任意の位相空間に対しても適用できる。位相空間論では閉包の開核がもとと一致する集合を正則開集合という。これはこのハイティング代数における二重否定で不変な集合と同じものである。正則開集合の全体は（完備）ブール代数を成す。これは古典論理が二重否定によって直観主義論理に埋め込めるというグリベンコの定理に対応している。

直観主義論理の双対^{[注 1]}は双対直観論理（英: dual-intuitionistic logic）である^[3]。双対直観論理は矛盾許容論理の一種であり、ブラジリアン論理（英: Brazilian logic）、反直観主義論理（英: anti-intuitionistic logic）などと呼ばれる論理と対応している^[4]。

直観主義論理から爆発原理（英語版）の公理を取り除いたものは最小論理（英語版）として知られる。

クルト・ゲーデルは1932年に直観主義論理が多値論理ではないことを証明した。（#ハイティング代数意味論は直観主義論理の"無限多値論理"としての解釈の一種と見られる。）

任意の有限ハイティング代数でブール代数でないものは（意味論的に）中間論理を定める。他方で、純粋な直観主義論理における論理式の妥当性は、特定のハイティング代数に結びついたものではなく、あらゆるハイティング代数に関係している。

直観主義命題論理の論理式は次のように様相命題論理S4の論理式に翻訳できる：

またこれにより直観主義論理を模倣できる^[5]。すなわち翻訳された論理式が様相命題論理S4で妥当であることと、翻訳前の論理式が直観主義命題論理IPCで妥当であることは同値である。上のような変換はゲーデル＝マッキンゼー＝タルスキ変換と呼ばれる。

様相論理S4の直観主義版は構成的様相論理CS4と呼ばれる^[6]。

カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。^[6]

• BHK解釈（英語版）
• 直観主義的型理論（英語版）
• 直観主義 (数学の哲学)
• 中間論理
• 線形論理
• 構成的証明（英語版）
• カリー＝ハワード対応
• 計算可能性論理（英語版）
• ゲーム意味論
• Smooth infinitesimal analysis（英語版）