とりあえず1周目
まえおき
定理証明手習いは"The Little Prover"の翻訳版です。出版社さんのページはこちら。物理本のみ、電子書籍のみ、両方の3つがあります。
本書の特徴は↑のページに簡潔に書かれているので、子の記事よりもそちらを読んだ方が良いのではと思います。
また、正誤情報があります。2つほど。1つ目のatomの方は先に知っておいた方が混乱がなくて良いでしょう。この分量で2つしかないのはすごい少ないと思う。
感想
さて、本書はSchemerシリーズ？のうちの一冊のようです。この本を読むためにLispの深い知識はそれほど必要ないですが、基本的な文法は本文中では特に説明されないのでそのレベルは事前に知っていた方が良いです。私はlisp方言のひとつを使ったことがあるので基本的な書き方は知っていますが、正しいlisperではないので（C言語風のシンタックスシュガーがあったので殆どそっちで書いていたほど）lisp言語的に不明な点は都度調べていました。
また、定理証明手習い+感想で検索したところ、こちらの記事がhitしました。読み進めていく過程の記事もあるので、詰まった部分があったら参考にすると良いかも…（私はそれら記事は未読）
http://kb84tkhr.hatenablog.com/entry/2017/12/30/170715
1周読んだだけで理解できるとは思っていないのですが、私の現時点での理解では与えられた主張を公理や証明済み定理を使って証明をしていく。証明とは最終的に`tで終わることを示すことで、恒真式だと考えれば良さそう。いくつかの法則を使えば、式を値まで評価せずに構文的な対応関係だけから簡約化が出来る。これはある意味で遅延評価的であって、最終的に値まで評価済みの場合は関数を適用するなどをしている。
基本的には記述の置き換えの形で証明を進めていくので、式変形を追うのはそれほど大変ではない。ただし、過去の定理等を覚えてない場合は都度読みに戻らないといけない（私はそうでした）が。
中盤から後半で再帰や帰納法を使うようになっていくが、この時点で前半の理解があいまいだと辛くなってくるので、必要なら前の章に戻って読み直すと良さそう。突然式が爆発的に増えるときは大体帰納法の式展開なのでそのページにしるしをつけて見直すと良さそう。式のミスはないので、じっくり置き換えて変換していけば正しい変形が出来るはずです。
前提を作るのは8章以降になるので、そこまでは与えられた前提に対して黙々と証明をしていきます。もくもくもくもく。。。
よくある？論理学の本で最初から全てを与えられていく形式ではなく、手を動かしながら一つずつ証明をこなしていくことで理解を深めていく感じですね。連言は8章、含意は9章で言葉が出てきますが、そこまでそういったことを意識せずにやってました。いわれてみれば、そうだな…と。
あと、この本は索引が凄いことになってます。注釈書かれている言葉が索引に入ってたり（普通はないと思う）。面白いのでちょっと眺めてみてください。困ったら索引から引けると思うので、困ったら索引を見ましょう。 また、本文は青と赤の色が使われている箇所があり、今どこに注目すればよいかが分かりやすいです。印刷も見やすい。あと表紙のゾウ？が可愛いですね。
また、最近興味が出てきた形式手法の証明はこの定理証明手習いで得たものが活きるのではと思っています（まだわからない。あとこの本をやってから形式手法に興味が出てきたので鶏と卵の関係）
と、とりとめもなく書いてしまいましたが、とても良書でした。本のタイトルからは自分にとってとても遠い本なのでは？と思っていたのですが、なんだかんだで一気に読み切ってしまいました（逆に、間をあけて読むのは難しいですが…忘れてしまうので）
まだ理解が浅いので、もう少し理解が深まったところでまた感想を書くかもしれません。呟くだけかもしれないけど。
