書名『証明論』だと思っていたら、もとは『数学基礎論』だったのか。 数学基礎論 (1974年) (現代数学講座〈1〉) http://www.amazon.co.jp/dp/B000JA152S 証明論入門―数学基礎論改題― （1988年02月） http://www.kyoritsu-pub.co.jp/bookdetail/9784320014060…

新しい本棚写真を撮って追加したほうがいい気がする（see 本棚写真もあてにならない - 檜山正幸のキマイラ飼育記 メモ編）。2014年の本棚写真 http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%CB%DC%C3%AA%5D は、http://www.chimaira.org/boo…

計算科学 -- 型付きラムダ計算とデカルト閉圏 論理 -- 自然演繹とシーケント計算 それらを結ぶのが多圏の絵算。どうやって結ぶのか： デカルト閉圏（一般には非対称モノイド閉圏）と厳密多圏の対応を作る。 自然演繹は絵算と同一視する。つまり、自然演繹の…

今日は画像だけ。いずれ本編で説明する機会があるかも。

makeはしょうもない所があるソフトウェアだが、使わざるを得ない。makeのルール（のヘッダ行部分）をシーケントと解釈できそうな気はする。T1 ... Tm : P1 ... Pn が、P1 ... Pn ⇒ T1 ... Tm。命題変数＝基本命題は、構文的には名前となる。その名前を論理式…

次のリンクで、本棚の写真をみることが出来る。 http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%CB%DC%C3%AA%5D だが、これで全部ではない。写真でいくら探してもない本が実物としてけっこうたくさん見つかった。最近買ったものではない。一…

movieismって“宗教”があるらしい。 https://www.facebook.com/Movieism-237717159625751/ Movieism - A religion that believes that when you die you then get resurrected in a movie that you have seen while living. resurrected 復活を遂げる 現世で…