直観主義論理

二重否定は肯定にならない

排中律は公理ではない

ChatGPT.icon

直観主義論理の証明過程を「プログラム」とみなし，命題を「型」と見なす対応関係。

これにより，論理の証明技術が型付きラムダ計算や関数型言語の型システム設計に応用された。

ランバッハやラムダ計算の研究は，直観主義論理で必須の「構成的証明」をモデル化する手段として発展。

プログラムの意味論（セマンティクス）を形式的に扱う基盤となった。

型理論と証明支援系

マーチン＝ローフ型理論（MLTT）など，直観主義論理をベースにした型理論が構築され，Coq, Agda といった証明支援系の核に。

これらは「プログラムの正当性を論理的に保証」する手段として，形式手法や安全性検証に用いられる。

関数型プログラミング言語

Haskell, OCaml, F# などの関数型言語は，直観主義論理的な型システム（例えば代数的データ型やモナド）をそのまま採用。

プログラムを「証明的に」（副作用を抑えつつ）構築・検証する設計思想が浸透。