3.3.4 答え合わせと 3.4 排中律と直観主義論理から
「計算可能であること」と「直観主義論理に収まっていること」はイコールか？
イエス
takezaki.icon 古典論理を使った証明も、その正しさが「計算できている」ように見えるのですが？
型チェックしているだけ。具体的に項を返さないという意味で「計算可能」ではない。
ebi_chan.icon 結局1つの回で全員読んでもらうのはほぼ無理ってことがわかってきたので、次からは1番上から始めないようにしようかな
ebi_chan.icon 最後kakkunさんだったということをメモしておく
練習問題
3.4.3
3.5.4
3.6.4