直観主義論理 (intuitionistic logic )
いま、A＝「円周率πの中に、７が20回連続して現れる」
B＝「円周率πの中に、７が19回連続して現れる」とすると、
A⊃B
は誰でも論理的に正しいと認めるだろう。
しかし、古典論理の法則（A⊃B≡¬A∨B）にしたがって、これを
¬A∨B
と言い換えたなら、これが正しいとは思えないだろう。
（Dirk van Dalen, Intuitionistic Logic から）
古典論理は、「命題は真であるか偽であるかのどちらかである」という前提（二値原理）に基づいている。
ブロウエル（Brouwer）は、カントの直観概念
（カントにおいて「直観」とは時間と空間という感性の形式のもとで見たり聞いたりする感覚作用を意味する）、
特に時間の直観に基づいて、
「無限」に関する扱いを制限し、人間が実際に構成できる範囲内で、論理の妥当性を考えようとした。
したがって、直観主義においては、「ある命題かその命題の否定かのどちらかが必ず真である」という排中律（A∨¬A）は認められない。
また、Aではないことが真ではないからといって、Aが真であるとは言えないから、二重否定の法則（¬¬A⊃A）も認められない。
（したがって背理法の使用も制限される。）
直観主義において、「真」であるとは、「証明される」ことであり、
否定（¬A）は、「Aが真（＝証明される）ならば矛盾が生じる」（A⊃人）と定義される。
直観主義論理の公理系
ブロウエルの主張を形式化し、最初に直観主義の公理系を立てたのは、ハイティング（Heyting）である。
その体系の基本は、ラッセル/ホッワイトヘッド『Principia Mathamtica』と同じだが、
派生記号（被定義記号）は、原始記号として扱われ、公理には次の11個が採用されている。
1. p⊃(p・p)
2. (p・q)⊃(q・p)
3. (p⊃q)⊃[(p・r)⊃(q・r)]
4. [(p⊃q)・(q⊃r)]⊃(p⊃r)
5. q⊃(p⊃q)
6. [p・(p⊃q)]⊃q
7. p⊃(p∨q)
8. (p∨q)⊃(q∨p)
9. [(p⊃r)・(q⊃r)]⊃[(p∨q)⊃r]
10. ¬p⊃(p⊃q)
11. [(p⊃q)・(p⊃¬q)]⊃¬p
（引用は、W.&M. Kneale, The Development of Logic から）
自然演繹（ゲンツェン）の公理系（NJ）
古典論理の公理系NKから二重否定の除去法則を除いたものが直観主義の公理系NJである。
自然演繹（NK）の公理系（再掲）
Aを仮定してBなら、Aを消去して、A⊃B （演繹定理）
AとA⊃Bから、B （MP）
AとBから、A∧B
A∧Bから、A および、A∧Bから、B
Aから、A∨B および、Bから、A∨B
Aを仮定してC、かつBを仮定してCならば、AとBを消去して新たにA∨Bを仮定して、C
Aを仮定して人（矛盾）なら、Aを消去して、¬A （背理法）
Aと¬Aから、人（矛盾）
人（矛盾）から、D（任意の命題）
¬¬Aから、A （二重否定の除去法則）
NKの証明図
上の推理規則を図にすると（上が記号を入れる規則、下が取る規則。「…」は途中省略の意味）
| A … B A⊃B |
A B A∧B |
A B A∨B A∨B |
A … 人 ¬A |
||
| A A⊃B B |
A∧B A∧B A B |
A B … … A∨B C C C |
A ¬A 人 |
人 D |
¬¬A A |
上の青のイタリック を除いたものが直観主義の公理系NJである。
四列目は、直観主義における否定の定義¬A≡A⊃人を表現している。
否定（¬A）は、直観主義では「Aならば矛盾」（A⊃人）と定義されるから、
Ｂに人を（またA⊃人に¬Aを）代入すれば、一列目と四列目は同じになる。
また排中律を認めないということと二重否定の除去法則を認めないということは同じである。
なぜなら、排中律を認めれば、二重否定の除去法則が導かれるし、
¬A ¬¬A
人
A∨¬A A A
A
¬¬A⊃A
逆に、二重否定の除去法則を認めれば、排中律が導かれる、からである。
A
A∨¬A ¬（A∨¬A）
人
¬A
A∨¬A ¬（A∨¬A）
人
¬¬（A∨¬A）
A∨¬A
したがって、六列目の除去は、直観主義では排中律が認められないことを意味している。
問１a
ド・モルガンの法則の一つ ¬（A∧B）⊃（¬A∨¬B）
が直観主義では証明できないことを示しなさい。
問１b
¬¬¬A⊃¬A の証明図を書きなさい。
反証モデル
<W, R, V> （クリプキ・モデル）
Wは世界（知識状態）の集合
Rは次のような世界間の到達関係（accessibility）
w1Rw1 （反射関係）
w1Rw2 かつ w2Rw3 ならば w1Rw3 （推移関係）
V は次の付値関数
（→は断定記号の代用 w→pは世界ｗにおいてｐが成り立つ（証明されうる）ということ）
(0) w→p かつ wRw' ならば w'→p
(1) w→p∧q ⇔ w→p かつ w→q
(2) w→p∨q ⇔ w→p または w→q
(3) w→p⊃q ⇔ wRw' である全ての w' において
w'→p ならば w'→q
(4) w→¬p ⇔ wRw' である全ての w' において
w'→p でない
（「w→¬p」と「w'→p でない」とは意味が全く違う。
「w→¬p」は「その時点以降で p が証明されたら矛盾が生じる（証明されることはあり得ない）」ということだが、
「w'→p でない」というのは「w'の時点で
p は証明できない」といことだから
後の w'' で p が証明される（w'' →p）ことはありうる。）
反射的かつ推移的な関係ということは、様相論理におけるS4と同じである。
その意味では、直観主義におけるA⊃Bは□（A⊃B）、¬Aは□¬Aと読み替えることが出来る。
例１
A∨¬A の反証モデル
W＝｛ w1, w2 ｝, R={ w1Rw1, w1Rw2, w2Rw2}, w2→p （すなわち V(p, w1)=0, V(p, w2)=1）とする。
これは w1 で p は証明できなかったが、w2 で p が証明できたというモデルである。
この時、w1→p でない、かつ w1→¬p でない（w1 で p が証明されたら矛盾が生じるということはない）から
w1→p∨¬p ではない（w1 では p∨¬p は成り立たない）。
問２
第二対偶法則（¬A⊃¬B）⊃（B⊃A）の反証モデルを作りなさい。
タブローによる分析
基本的には様相論理の応用だが、¬A aではなく、A -a と表記する。
世界a において¬Aが真でなくてもAが偽であることがありうるからである。
A +a Aは世界（知識状態）aで真
A -a Aは世界（知識状態）aで偽
| A∧B +a ｜ A +a B +a |
A∧B -a ／＼ A -a B -a |
| A∨B +a ／＼ A +a B +a |
A∨B -a ｜ A -a B -a |
| A⊃B +a aRb ／＼ A -b B +b |
A⊃B -a | aRb A +b B -b |
| ¬A +a aRb ｜ A -b |
¬A -a ｜ aRb A +b |
| p +a aRb | p +b （遺伝法則） |
p -a (この分析規則は存在しない) |
１）与えられた式Aが a において成り立たないと仮定して、A
-a から分析を始める。
２）上の二行（∧と∨）から先に分析する。
３）A⊃B -a と ¬A -a においては、b には新しい文字（数字）を入れる。
４）A⊃B +a と ¬A +a では、全ての到達可能な世界で矛盾が生じないことを確かめる。
（到達関係は、反射的 aRa、かつ推移的 aRb、bRc → aRc）
５）同じ枝で p +a と p -a が生じたら×（矛盾）をつけて分析を止める（pは要素命題）。
６）矛盾が生じない枝が一つでもあれば、妥当式ではない。
（その枝で、与式を偽にするモデルが作れる。）
例２a
p⊃¬¬p -0
｜
0R0
0R1
p +1
¬¬p -1
｜
1R1
1R2
¬p +2
2R2
0R2
｜
p -2
｜
p +2
×
ゆえに与式は妥当式
例２b p⊃q→¬p∨q
p⊃q +0
¬p∨q -0
0R0
｜
¬p -0
q -0
｜
0R1
p +1
1R1
／＼
p -0 q +0
／＼ ×
p -1 q +1
× ○
ゆえに与式は妥当式ではない
○のついた枝で
W＝｛ w0, w1 ｝,
R={ w0Rw0, w0Rw1, w1Rw1},
V(p, w0)=V(q, w0)=0, V(p, w1)=V(q, w1)=1
w0から到達可能な全ての世界（w0, w1）で pの値が偽またはqの値が真 だから p⊃qはw0で真、
w1でpが真だからw0で¬pは偽、w0でqも偽だから、w0で¬p∨qは偽、
すなわちw0でp⊃q→¬p∨qは偽となる。
したがって、直観主義論理では、（A⊃B）≡（¬A∨B）は妥当式ではない。
問３
例２aの逆 ¬¬p⊃p をタブローで分析しなさい。