自然演繹の証明図をひたすら書く教材を作成しました。
この教材では自然演繹の証明図を書く問題を100題提出します。 しかし、数理論理学は、証明図を書く学問ではありません。 では、なぜ100題ノックを世に出すのかという問いは自然なものです。 その答えは、証明図を書くことに脳のリソースを使わないでいいことで、 証明図・証明とは何かを概念的に思考する余裕が生じると考えたからです。
ぜひ、挑戦してみてください。
なお、バージョンアップ情報をstoresjpのメールマガジンよりお知らせすることがあります。
はじめにより
数理論理学は、 証明図を書く学問ではない。 論理を、とくに数学で使われる論理を研究する数学の一分野である。 そのなかで証明図とは、証明を記号化したものであり、 つまり数学の対象として図形のように扱えるようにしている。 幾何学が、図形を描く学問でなく、図形について考察する学問であるのと同様なのであろう。
数理論理学の歴史は、 大雑把には数学、特にその証明自体を数学的対象として扱うことから始まった。 数学的対象として扱うには、 命題や証明を記号化して、 先に述べたように図形のように扱えるとよい。
さて、 本稿では証明図を書く問題を100題提出する。 先ほど「数理論理学は、証明図を書く学問ではない」と述べたが、 では、なぜ100題ノックを世に出すのか。 それは証明図を書くことに脳のリソースを使わないでいいことで、 証明図・証明とは何かを概念的に思考する余裕が生じると考えるからである。
したがって本稿は、 数理論理学を学んでいるものの証明図を書くことに苦労を感じ、 肝心の理論的な理解に困難を抱える数理論理学の初学者を念頭に書かれている。
証明図を書くには、 証明図の定義に従って規則を並べていくことに徹することになる。 よってこの問題への唯一のアプローチは、 考えないことである。 もちろん、 シークエント計算で先に証明するとか否定翻訳とかといった難しい問題を解く手法も存在するし、 それらを用いて解いてくださっても構わない。 しかし、 本稿の狙いはあくまでも、 考えないでも自然演繹の証明図を書けるようになる点にある。
本稿には、 最小命題論理、直観主義命題論理、古典命題論理、古典述語論理の四つの論理体系が出てくる。 各章内の「演習」の節では、各体系で証明可能な(メタ)論理式を紹介する。 その証明図を書いていただこうという趣旨である。 演習問題は四つの体系を合わせて100個の論理式からなる。 ただし、 各章の最初に「例題」という節があり、 そこでは典型的な証明図を例示している。
演習問題に対して、 「回答例」という章が設けられているが、 全ての問題に回答を付しているわけではない。 それを求める方向けに、 論計舎で採点・解説をする講座が存在する。 また、 「例」となっているのは一つの論理式に対して複数の正当な証明図が存在するためである。
目次
・はじめに
・本稿の手引き
・最小命題論理
・直観主義命題論理
・古典述語論理
・回答例
・おわりに
--------
・メールマガジンにご登録いただきますと新しい版の情報をお届けします。
--------
第二版の変更点 (2023/01/15)
・回答例が正しい導出図でないものを正しいものに修正しました。
・演習098の括弧を補いました。
--------
第三版の変更点 (2023/01/21)
・回答例が正しい導出図でないものを正しいものに修正しました。
--------
第四版の変更点 (2023/06/01)
・出題した論理式が意図したものでなかったので変更しました。
--------
第五版の変更点 (2023/06/01)
・問97のtypoを修正しました。