- 「直観主義論理の「自然さ」(1) 自然演繹」
直観主義論理の自然演繹では導入則と除去則とが相補的な関係になっている。 - 「直観主義論理の「自然さ」(2) シーケント計算 」
直観主義論理の自然演繹体系を変形すると直観主義のシーケント計算の体系が得られる。 - 「直観主義論理の「自然さ」(3)古典論理のシーケント計算と自然演繹」
直観主義論理の演繹体系に規則を追加して結論に複数の論理式を置けるようにすると古典論理の体系になる。 - 「直観主義論理のカリー・ハワード対応」
直観主義論理の自然演繹と型付きラムダ計算との対応関係の説明。 - 「call/ccと古典論理のカリー・ハワード対応」
ラベル付きブロック構文とcall/ccの説明。型付きラムダ計算にcall/ccを追加したものは、直観主義論理+(¬A→A)→A = 古典論理に対応する。 - 「古典論理のカリー・ハワード対応のためのラムダ計算」
λμ計算(の変種)の説明。ラムダ計算を古典論理に対応するように拡張したもの。 - 「古典論理のカリー・ハワード対応での証明の書き換えと簡約」
λμ計算についての続き。ジャンプ構文の簡約規則と証明図の変形との対応関係。 - 「シーケント計算に対応する計算体系を考えてみる」
自然演繹⇔型付きラムダ計算と同様の対応を、シーケント計算について考える。シーケント計算⇔?? 。古典論理に関する部分は不充分。
