直観主義論理 （ちょっかんしゅぎろんり、英 : intuitionistic logic ）または直観論理 （ちょっかんろんり）、あるいは構成的論理 （こうせいてきろんり、英 : constructive logic ）とは、ある種の論理体系であり、伝統的な真理値 の概念が構成的証明 の概念に置き換わっている点で古典論理 とは異なる。例えば古典論理では、全ての論理式 に真か偽の真理値 (
{
⊤ ⊤ -->
,
⊥ ⊥ -->
}
{\displaystyle \{\top ,\bot \}}
証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律 や二重否定除去 が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。
直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なブール代数値意味論 を写しとったものでブール代数 の代わりにハイティング代数 を用いる。別の意味論ではクリプキ・モデル を用いる。
直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性 を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義 のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。
形式化された直観主義論理はアレン・ハイティング によってヤン・ブラウワー の直観主義 プログラムの形式的な基礎として発展せられたものである。
Rieger–Nishimura束のハッセ図。これのノードは変数をひとつだけ持つ命題論理式の直観主義的な同値性による同値類で、その順序は直観主義的な含意から誘導されるものである。 直観主義論理の論理式の構文は古典命題論理 や古典述語論理 と類似である。しかしながら、直観主義的な論理結合子 は、古典論理 におけるように、他の論理結合子を用いて定義することはできない。（そのため
{
→ → -->
,
⊥ ⊥ -->
}
{\displaystyle \{\to ,\bot \}}
{
∧ ∧ -->
,
¬ ¬ -->
}
{\displaystyle \{\wedge ,\neg \}}
{
∨ ∨ -->
,
¬ ¬ -->
}
{\displaystyle \{\vee ,\neg \}}
→ → -->
,
∧ ∧ -->
,
∨ ∨ -->
,
⊥ ⊥ -->
{\displaystyle \to ,\wedge ,\vee ,\bot }
¬ ¬ -->
A
{\displaystyle \neg A}
A
→ → -->
⊥ ⊥ -->
{\displaystyle A\to \bot }
∃ ∃ -->
,
∀ ∀ -->
{\displaystyle \exists ,\forall }
多くの古典論理の恒真式 は直観主義的には証明できない。排中律
p
∨ ∨ -->
¬ ¬ -->
p
{\displaystyle p\vee \neg p}
パースの法則
(
(
p
→ → -->
q
)
→ → -->
p
)
→ → -->
p
{\displaystyle ((p\to q)\to p)\to p}
二重否定除去
¬ ¬ -->
¬ ¬ -->
p
→ → -->
p
{\displaystyle \neg \neg p\to p}
p
→ → -->
¬ ¬ -->
¬ ¬ -->
p
{\displaystyle p\to \neg \neg p}
¬ ¬ -->
¬ ¬ -->
¬ ¬ -->
p
→ → -->
¬ ¬ -->
p
{\displaystyle \neg \neg \neg p\to \neg p}
p
∨ ∨ -->
¬ ¬ -->
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 }
ψ ψ -->
→ → -->
ϕ ϕ -->
{\displaystyle \psi \to \phi }
ψ ψ -->
→ → -->
(
∀ ∀ -->
x
ϕ ϕ -->
)
{\displaystyle \psi \to (\forall x\ \phi )}
x
{\displaystyle x}
ψ ψ -->
{\displaystyle \psi }
∃ ∃ -->
{\displaystyle \exists }
ϕ ϕ -->
→ → -->
ψ ψ -->
{\displaystyle \phi \to \psi }
(
∃ ∃ -->
x
ϕ ϕ -->
)
→ → -->
ψ ψ -->
{\displaystyle (\exists x\ \phi )\to \psi }
x
{\displaystyle x}
ψ ψ -->
{\displaystyle \psi }
また次のものを公理図式に加える：
PRED-1:
(
∀ ∀ -->
x
ϕ ϕ -->
(
x
)
)
→ → -->
ϕ ϕ -->
(
t
)
{\displaystyle (\forall x\ \phi (x))\to \phi (t)}
t は
ϕ ϕ -->
{\displaystyle \phi }
x への代入について自由である (つまり t の中の変数記号は
ϕ ϕ -->
(
t
)
{\displaystyle \phi (t)}
PRED-2:
ϕ ϕ -->
(
t
)
→ → -->
(
∃ ∃ -->
x
ϕ ϕ -->
(
x
)
)
{\displaystyle \phi (t)\to (\exists x\ \phi (x))}
もし否定を表す結合子
¬ ¬ -->
{\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 }
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 }
(
ϕ ϕ -->
→ → -->
χ χ -->
)
∧ ∧ -->
(
χ χ -->
→ → -->
ϕ ϕ -->
)
{\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 )}
全称量化と存在量化：
(
∀ ∀ -->
x
ϕ ϕ -->
(
x
)
)
→ → -->
¬ ¬ -->
(
∃ ∃ -->
x
¬ ¬ -->
ϕ ϕ -->
(
x
)
)
{\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}
(
∃ ∃ -->
x
ϕ ϕ -->
(
x
)
)
→ → -->
¬ ¬ -->
(
∀ ∀ -->
x
¬ ¬ -->
ϕ ϕ -->
(
x
)
)
{\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}
(
∃ ∃ -->
x
¬ ¬ -->
ϕ ϕ -->
(
x
)
)
→ → -->
¬ ¬ -->
(
∀ ∀ -->
x
ϕ ϕ -->
(
x
)
)
{\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}
(
∀ ∀ -->
x
¬ ¬ -->
ϕ ϕ -->
(
x
)
)
↔ ↔ -->
¬ ¬ -->
(
∃ ∃ -->
x
ϕ ϕ -->
(
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 }
A
∧ ∧ -->
B
{\displaystyle A\wedge B}
A
{\displaystyle A}
B
{\displaystyle B}
⊤ ⊤ -->
{\displaystyle \top }
直観主義論理においても同様の完全性定理が成立するが、論理式の真理値はブール代数の代わりにハイティング代数の元を用いる。ブール代数はハイティング代数の特別な場合である。このとき論理式が直観主義論理で妥当であることと、任意のハイティング代数とその上で値を取る真理値割り当てに対して論理式の真理値が
⊤ ⊤ -->
{\displaystyle \top }
論理式が妥当であることを確かめる為には、ひとつのハイティング代数の上で調べれば十分であることが証明できる。そのハイティング代数は数直線
R
{\displaystyle \mathbb {R} }
[ 2]
∧ ∧ -->
{\displaystyle \wedge }
∨ ∨ -->
{\displaystyle \vee }
A
→ → -->
B
{\displaystyle A\to B}
i
n
t
(
A
c
∪ ∪ -->
B
)
{\displaystyle \mathrm {int} (A^{c}\cup B)}
A
{\displaystyle A}
B
{\displaystyle B}
内部 である。（これは古典論理における含意の演算の結果を開集合になるように調整したものである。様相論理の観点から見るとこれは必然性を外側に付けているのと同じことになる。）
⊥ ⊥ -->
{\displaystyle \bot }
∅ ∅ -->
{\displaystyle \varnothing }
⊤ ⊤ -->
{\displaystyle \top }
R
{\displaystyle \mathbb {R} }
¬ ¬ -->
A
{\displaystyle \neg A}
A
→ → -->
⊥ ⊥ -->
{\displaystyle A\to \bot }
A
{\displaystyle A}
外部 と一致する。この対応付けによって直観主義的に妥当な論理式はちょうど空間全体が割り当てられるものと一致する。[ 2]
例えば矛盾律
¬ ¬ -->
(
A
∧ ∧ -->
¬ ¬ -->
A
)
{\displaystyle \neg (A\wedge \neg A)}
X
{\displaystyle X}
A
{\displaystyle A}
¬ ¬ -->
(
A
∧ ∧ -->
¬ ¬ -->
A
)
{\displaystyle \neg (A\wedge \neg A)}
v
a
l
(
¬ ¬ -->
(
A
∧ ∧ -->
¬ ¬ -->
A
)
)
=
i
n
t
(
(
X
∧ ∧ -->
i
n
t
(
X
c
)
)
c
)
{\displaystyle \mathrm {val} (\neg (A\wedge \neg A))=\mathrm {int} ((X\wedge \mathrm {int} (X^{c}))^{c})}
位相空間論 によれば
i
n
t
(
X
c
)
{\displaystyle \mathrm {int} (X^{c})}
X
c
{\displaystyle X^{c}}
X
{\displaystyle X}
i
n
t
(
∅ ∅ -->
c
)
=
i
n
t
(
R
)
=
R
{\displaystyle \mathrm {int} (\varnothing ^{c})=\mathrm {int} (\mathbb {R} )=\mathbb {R} }
したがってこの論理式の付値は真であり、妥当であることが従う。
しかし排中律
A
∨ ∨ -->
¬ ¬ -->
A
{\displaystyle A\vee \neg A}
A
{\displaystyle A}
(
0
,
∞ ∞ -->
)
{\displaystyle (0,\infty )}
¬ ¬ -->
A
{\displaystyle \neg A}
(
− − -->
∞ ∞ -->
,
0
]
{\displaystyle (-\infty ,0]}
(
− − -->
∞ ∞ -->
,
0
)
{\displaystyle (-\infty ,0)}
(
0
,
∞ ∞ -->
)
{\displaystyle (0,\infty )}
(
− − -->
∞ ∞ -->
,
0
)
{\displaystyle (-\infty ,0)}
R
∖ ∖ -->
{
0
}
{\displaystyle \mathbb {R} \setminus \{0\}}
数直線からハイティング代数を作る上のやり方は任意の位相空間に対しても適用できる。位相空間論では閉包の開核がもとと一致する集合を正則開集合 という。これはこのハイティング代数における二重否定で不変な集合と同じものである。正則開集合の全体は（完備）ブール代数を成す。これは古典論理が二重否定によって直観主義論理に埋め込めるというグリベンコの定理 に対応している。
直観主義論理の双対[ 注 1] 英 : dual-intuitionistic logic ）である[ 3] 矛盾許容論理 の一種であり、ブラジリアン論理（英 : Brazilian logic ）、反直観主義論理（英 : anti-intuitionistic logic ）などと呼ばれる論理と対応している[ 4]
直観主義論理から爆発原理 （英語版 ） 最小論理 （英語版 ）
クルト・ゲーデル は1932年に直観主義論理が多値論理 ではないことを証明した。（#ハイティング代数意味論 は直観主義論理の"無限多値論理"としての解釈の一種と見られる。）
任意の有限ハイティング代数でブール代数でないものは（意味論的に）中間論理 を定める。他方で、純粋な直観主義論理における論理式の妥当性は、特定のハイティング代数に結びついたものではなく、あらゆるハイティング代数に関係している。
直観主義命題論理の論理式は次のように様相命題論理S4 の論理式に翻訳できる：
⊥ ⊥ -->
∗ ∗ -->
{\displaystyle \bot ^{*}}
=
⊥ ⊥ -->
{\displaystyle \ \bot }
A
∗ ∗ -->
{\displaystyle A^{*}}
=
◻ ◻ -->
A
if
A
is prime (a positive literal)
{\displaystyle \ \Box A\qquad {\hbox{if }}A{\hbox{ is prime (a positive literal)}}}
(
A
∧ ∧ -->
B
)
∗ ∗ -->
{\displaystyle (A\wedge B)^{*}}
=
A
∗ ∗ -->
∧ ∧ -->
B
∗ ∗ -->
{\displaystyle \ A^{*}\wedge B^{*}}
(
A
∨ ∨ -->
B
)
∗ ∗ -->
{\displaystyle (A\vee B)^{*}}
=
A
∗ ∗ -->
∨ ∨ -->
B
∗ ∗ -->
{\displaystyle \ A^{*}\vee B^{*}}
(
A
→ → -->
B
)
∗ ∗ -->
{\displaystyle (A\rightarrow B)^{*}}
=
◻ ◻ -->
(
A
∗ ∗ -->
→ → -->
B
∗ ∗ -->
)
{\displaystyle \ \Box (A^{*}\rightarrow B^{*})}
(
¬ ¬ -->
A
)
∗ ∗ -->
{\displaystyle (\neg A)^{*}}
=
◻ ◻ -->
(
¬ ¬ -->
(
A
∗ ∗ -->
)
)
since
¬ ¬ -->
A
:=
A
→ → -->
⊥ ⊥ -->
{\displaystyle \ \Box (\neg (A^{*}))\qquad {\hbox{since }}\neg A:=A\rightarrow \bot }
またこれにより直観主義論理を模倣できる[ 5] ゲーデル＝マッキンゼー＝タルスキ変換 と呼ばれる。
様相論理S4の直観主義版は構成的様相論理CS4と呼ばれる[ 6]
カリー＝ハワード対応 はIPCと直和と直積を持つ単純型付きラムダ計算 との間に拡張できる。[ 6]
^ ここでの双対はシークエント計算においての双対である。
^ Proof Theory by G. Takeuti, ISBN 0-444-10492-5
^ a b Sørensen, Morten Heine B; Paweł Urzyczyn (2006). Lectures on the Curry-Howard Isomorphism . Studies in Logic and the Foundations of Mathematics. Elsevier . p. 42. ISBN 0-444-52077-5
^ Urbas, Igor (1996-07-01). “Dual-Intuitionistic Logic” . Notre Dame Journal of Formal Logic 37 (3). doi :10.1305/ndjfl/1039886520 . ISSN 0029-4527 . https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-37/issue-3/Dual-Intuitionistic-Logic/10.1305/ndjfl/1039886520.full . ^ Aoyama, Hiroshi (2004). “LK, LJ, Dual Intuitionistic Logic, and Quantum Logic”. Notre Dame Journal of Formal Logic 45 (4): 193–213. doi :10.1305/ndjfl/1099238445 . ^ Lévy, Michel (2011年4月29日). “Logique modale propositionnelle S4 et logique intuitioniste propositionnelle ” (PDF). pp. 4–5. 2015年5月8日 閲覧。 ^ a b Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter. “Categorical and Kripke Semantics for Constructive S4 Modal Logic ” (PDF). 2015年5月8日 閲覧。
前原昭二 『数学基礎論 』財団法人放送大学教育振興会van Dalen, Dirk , 2001, "Intuitionistic Logic", in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic . Blackwell.Morten H. Sørensen, Paweł Urzyczyn, 2006, Lectures on the Curry-Howard Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.
W. A. Carnielli (with A. B.M. Brunner)."Anti-intuitionism and paraconsistency" . Journal of Applied Logic Volume 3, Issue 1, March 2005, pages 161-184.
![{\displaystyle (-\infty ,0]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0241c015ef4c611c9c9aeafb395e7c4a16178405)
