http://itpro.nikkeibp.co.jp/article/COLUMN/20070909/281498/?ST=developややブームに乗り遅れた(?)感もありますが、カリー・ハワード同型（のさわり）の話です。追記：直観主義論理＋二重否定の除去（¬¬Ａ⇒Ａ）だけから排中律（Ａ∨¬Ａ）を示す、などに興…