kt3k 日記

スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

何回目かの考究

shoenfield_book

ゼミで Shoenfield, Mathematical logic の 115p - 119p
を発表。後半をあまり予習してなかったので、後半がだいぶグダグダ
な感じになって、聞いてる人に申し訳ない感じの発表になった。
でも、前半で、lemma の条件で β(a, i) <= a - 1 という条件不要じゃないか?
とか、page116, line16 l, j の条件は、1 <= j < l <= c じゃないかとか
おもしろい(と思える)突っ込みがあって、楽しかったので、トータルOK

立ち話

DJ、FLASHer、考究仲間の(qre)さんと2時間ぐらい立ち話した。

今日は考究が途中で中断して、みんなでゾロゾロ歩いて、
コレを聞きに行った。ACL2という証明器で、quicksort がソートできている
事を証明するデモなんかを眺めた。Ruben Gamboa さんという人が実装したという、
ACL2(r)というACL2の拡張で、解析学の定理を証明した話の紹介が興味深かった。

考究では、論理以外の公理を持たない理論の中で、existential な論理式が定理である
ためには、その論理式の matrix のインスタンス達を or でつないだもののうちで、
quasi-toutology になるものが存在することが必要十分であるということ(棒読み)を証明した。
(consistency theorem とか、prenex operation の基本的性質が証明済みなので、そこまで
難しくない。)

shoenfield


後期授業

大学の後期授業が始まった。
幾何学Ⅱの授業に出た。

diff_form

(授業で利用されるオーパーツ)

授業後に友達の引っ越しを手伝った。

ジョン・ホートン・コンウェイ

だれも何も書かないのでなかなか充実しない wikipedia
ジョン・ホートン・コンウェイの項目をいろいろ書き足した。
調べているうちに、ソーマキューブを解いたのがコンウェイだと分かったり、
rack という代数系をかなり早いうちに議論していたのがコンウェイだと分かったり、
改めて活動の広さに驚いた。

johnconway

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。