直観主義論理

logiccomputer-sciencetype-theory

「証拠を構成しないと真とは言えない」という立場の論理。

プログラマ向けの一言

「存在する」と言うなら実際に作って見せろ、という論理。 古典論理では「存在しないと矛盾する、だから存在する」が通るが、直観主義では「実際に構成して見せて初めて存在する」。

古典論理との違い

// 古典論理: 排中律（P または ¬P は常に真）を認める
// 「素数は無限にある。なぜなら、有限だと仮定すると矛盾するから」
// → 矛盾を示せば OK。実際に素数を1つずつ構成する必要はない

// 直観主義論理: 排中律を仮定しない
// 「素数は無限にある」を示すには、任意の n に対して
// n 番目の素数を実際に構成するアルゴリズムを示す必要がある

// プログラマ的に言うと:
function classicalProof(): boolean {
  // 「P が偽だと矛盾する」→「P は真」
  // 背理法で存在を示すが、実際の値は得られない
  return true; // ... でも具体的な値は？
}

function constructiveProof(): { value: number; proof: string } {
  // 「P を満たす値を実際に構成する」
  return { value: 42, proof: "ここに具体的な構成がある" };
  // → 証明 = プログラム（値を計算して返す）
}

排中律と二重否定除去

// 古典論理で認められ、直観主義で認められないもの:

// 1. 排中律: P ∨ ¬P（P か not P のどちらか）
// 型で言うと: 任意の型 A に対して A | (A => never) が得られる
// → 直観主義では「A の値があるか、A が矛盾を導くか」の
//   どちらかを必ず決められるとは限らない

// 2. 二重否定除去: ¬¬P → P
// 型で言うと: ((A => never) => never) => A
// → 「A がないと矛盾する」ことから A を取り出す
function doubleNeg<A>(proof: (notA: (a: A) => never) => never): A {
  // ... これを実装する方法がない！
  // 矛盾を示せても、A の具体的な値は得られない
  throw "impossible in constructive logic";
}

// 逆（P → ¬¬P）は直観主義でも成り立つ:
function introDoubleNeg<A>(a: A): (notA: (a: A) => never) => never {
  return (notA) => notA(a); // A の値があるなら、¬A に渡せば矛盾する
}

なぜプログラミングに関係するか

// カリー=ハワード対応で:
// 命題 = 型、証明 = プログラム
//
// 直観主義の証明 = 実行可能なプログラム
// 古典論理の証明 = 実行可能とは限らない（存在は示すが構成しない）
//
// だから型システムは本質的に直観主義論理に対応する
// → Coq, Agda, Lean などの定理証明系はすべて直観主義論理ベース
// → 「証明する」=「プログラムを書く」が成り立つのは直観主義だから

押さえどころ（カード化候補）

関連

Graph

Backlinks