- 480 名前：470 mailto:sage [2005/05/30(月) 22:14:29 ]
- 通常の数学で、等号の公理といえば、
（= 導入） ｔ が項なら ├ ｔ=ｔ
あるいは同じことだが、
（= 導入)' ｓ と ｔ が同一の項なら ├ ｓ=ｔ
という推論規則と
（= 消去） ｓ=ｔ, Ｐ(ｓ) ├ Ｐ(ｔ)
という２つの推論規則を仮定する（もちろん他の流儀もあるが）。
このとき、上のつの推論規則はある意味で“対”になっている。
それは、（= 消去）で“消去”される等式 ｓ=ｔ を（= 導入）
の前提「ｓ と ｔ が同一の項」で置き換えると、
ｓ と ｔ が同一の項, Ｐ(ｓ) ├ Ｐ(ｔ)
あるいは同じことだが
Ｐ(ｔ) ├ Ｐ(ｔ)
となって「当たり前の結論」が得られる。このように、消去規則の消去
すべき式を導入規則の前提で置き換えたとき、当たり前の結論しか得られ
ないという性質は、等号に関する推論規則だけでなく、自然推論における
論理記号 ∧ ∨ ⇒ ⊥ ∀ ∃ の推論規則についても成り立ち、このことが
直観主義論理をある意味で「特徴づけて」いる。（これに対し、¬ に関す
る古典論理の推論規則はこのような性質を持たない。）
|
 |
