ゲンツェンとの関係 あまり知られていないがシーケント計算や自然演繹を考え出したゲンツェンの最初の論文はパウル・ヘルツの体系に関する結果である1。ヘルツは特にシーケント、カット規則、弱化規則に関してゲンツェンに影響を与えている。 この記事ではヘ…

Haskell等で使われるLens(の一般形)1は実は論理学とも深い関係がある。Lensの構造に関する研究の(おそらく)最も最初のものはゲーデルのディアレクティカ解釈の研究である2。 ゲーデルのディアレクティカ解釈とは直観主義算術から量化子なしの有限型算術 Tへ…