論計舎の活動を支援して下さる方向けの寄付。商品の発送はございません。頂いた支援金は全て運営費にあてさせていただきます。

論計舎の活動を支援して下さる方向けの寄付。商品の発送はございません。頂いた支援金は全て運営費にあてさせていただきます。

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

与えられた充足不可能な論理式の反例をひたすら構成する教材を作成しました。この教材では100個の充足不可能な論理式を紹介します。反例を構成することは日々の数学の証明において必要とされる上に、構成したモデルがきちんと反例になっていることを論証することは、数学の論証それ自体の訓練になると信じて世に出します。ぜひ、挑戦してみてください。なお、バージョンアップ情報をstoresjpのメールマガジンよりお知らせすることがあります。はじめにより論理式の意味的な正しさを考えることを意味論 semantics という。意味論には、記号の内容を無視して記号列がなす証明が正しい証明かどうかでその意味的正しさを判断する証明によるアプローチと、モデルと呼ばれる論理体系の意味内容を反映した数学的対象を構成して論理式の意味的正しさを判断するモデルを使ったアプローチが存在する。先に公開した『自然演繹100本ノック』では、前者の証明論を紹介した。本稿で紹介するのは、後者の伝統的に意味論と言われていたモデルを用いたアプローチである。証明論が与えられた論理式が正しいことを保証するのを得意とする反面、モデルを用いると与えられた論理式が成立しない場合があることを示すことが容易である。このことは、数理論理学が、数学で使われる論理を研究する数学であることを鑑みると、日々の数学において端的に数学の定理を得るためには証明をする必要があるのに対して予想を否定するには反例を一つでも挙げればよいことと対応する。さて、本稿では反例を構成する問題を100題提示する。『自然演繹100本ノック』の冒頭で数理論理学が証明図を書く学問でないと述べたように、数理論理学は反例モデルを構成する学問ではない。しかしながら、モデルを構成することは日々、数理論理学の定理を証明する中で必要とされる上に、構成したモデルがきちんと反例になっていることを論証することは、数学の論証それ自体の訓練になるものと想像する。したがって本稿は、数理論理学を通して数学の考え方を理論においても実践においても身につけることを目指されるある程度の数理論理学への習熟を持った学習者に向けられている。本稿には、直観主義命題論理、様相命題論理、古典述語論理、関連性論理の4つの論理体系が出てくる。各章内の「演習」の節では、各体系で証明不可能な（メタ）論理式を紹介する。その論理式を非妥当にするモデルを構成していただこうという趣旨である。演習問題は4つの体系を合わせて100個の論理式からなる。ただし、各章の最初に「例題」という節があり、そこでは反例モデルと論証の仕方を例示している。回答を求める方向けに、論計舎で添削・解説をする講座を検討している。目次・はじめに・本稿の手引き・直観主義命題論理・古典述語論理・様相論理・関連性論理・回答例・おわりに--------

論と計の門を叩こうとする人に少しでも適切な門を紹介したい。そう考えたのが本稿の執筆のきっかけです。論計舎の活動の中で数学の学び方や数理論理学とはなにかといった話、そして何よりおすすめの教科書・テキストの提示が、適切な門の提示であると考え、本稿はこの考えに従った構成にしました。しかし、内容的に新規ではありません。既に多くの人が語ってきたところを短く端的にまとめることを心がけました。第1章では、数理論理学は数学の一分野であるという立場から前提としての数学の学び方に関する筆者の考えを紹介しています。第2章は数理論理学とは何かへの説明をしています。ここでは可能なかぎり、読者のみなさんの関心を想像しながら、歴史の説明と重要な定理・成果を概略的に解説するように心がけました。第3章と第4章はひとまとまりに考えられます。この二つの章がおすすめのテキストの紹介とそれらがどうおすすめであるかとかどう使うべきかという話を担います。筆者自身の学びが読者のみなさんに還元されて、さらにはより多くの方が論と計の科学の、つまり数理論理学の門を叩いてくださればと願います。論計舎の紹介論計舎（ろんけいしゃ）は、 数理「論」理学と「計」算機科学を主軸としたオンライン私塾です。目次1. 数学の学び方 §1.1 テキストについて §1.2 輪読・輪講という学び方 §1.3 質問すること2. 数理論理学の概略と特徴 §2.2 数理論理学とは §2.3 区別の重要性3. スターターキット的ブックリスト4. 上掲書への書評5. 論計舎の講座紹介バージョン: 第一版ページ数: 13--------・メールマガジンにご登録いただきますと新しい版の情報をお届けします。

論計舎（ろんけいしゃ）は、 数理論理学と計算機科学を主軸とした オンライン私塾です。論計舎は数理論理学と計算機科学を「論と計の科学」として掲げそれを伝え広めることをミッションとしています。そこには数学的な原理が背景にあり、論理・計算を必要とするすべての人に益するであろうという思いが動機にあります。## Description なお、販売後も適宜、アップデートしていく予定です。アップデートは本web shopのメールマガジンにてお伝えします。最新版は、購入時のメールアドレスと注文番号をご連絡いただければ、お送りします。一階述語論理に健全性・完全性の証明をしたことがある方を念頭に、二つの不完全性定理の証明をできるだけ詳細にお伝えしつつ、その証明に最短で到達する講義です。構成は、以下からなります。* オリジナルテキスト* YouTube上限定公開の講義動画* 講義で用いたスライドまた、テキストの講義対応部分から講義動画へリンクされるようになっております。省略されがちなコード化の議論などをある程度は丁寧に紹介しますが、定理の性質上、無尽蔵に丁寧さを増すことができますので、適切に区切ってあります。## Speaker 川井 新 (Shin Quawai)論計舎主催・講師。 論理と計算の関わりに関心をもち、在野研究者として活躍中。他に哲学的論理学も専門とする。RIMS共同研究にて口頭発表2回。論理学友の会発起人。指導実績のある分野に、線形代数、微分積分学、数理論理学。ウィスキーと珈琲を好む。## Requirements一階述語論理の健全性・完全性の証明の理解。## Course Objectives数理論理学の基本定理で一つの大きな達成である、ゲーデルの不完全性定理を理解する。ここでいう理解とは、背後の基本的な考え方・発想および数学的な技法を含むものである。この技法は、不完全性定理にかぎらず、チューリングおよびチャーチそれぞれによる実行的に解けない数学の問題の存在を示した業績などでも使われたものである。## Schedule1. Historical Backgrounds 2. Proof Theory: Quick Installation 3. Proof Theory: Details and Examples4. Computability: Quick Installation 5. Church-Turing Thesis6. An Introduction to Incompleteness 7. The First Incompleteness Theorem8. The Secound Incompleteness Theorem## Resources### Main Text* 本商品### Other Texts* 鹿島亮『数理論理学』朝倉出版、2009* Cooper, S. Barry. Computability theory. Chapman and Hall/CRC, 2017.* 新井敏康『数学基礎論 増補版』東大出版、2021* 菊池誠『不完全性定理』共立出版、2014* トルケル・フランセーン『ゲーデルの定理 利用と御用の不完全ガイド』みすず出版、2011### Further reading on Incompleteness* ゲーデル著、林晋、八杉満利子、訳・解説、『不完全性定理』岩波書店* Boolos, George. "Gödel's second incompleteness theorem explained in words of one syllable." Mind (1994): 1-3.* Boolos, George. "A New Proof of the Gödel Incompleteness Theorem." Notices Am. Math. Soc. 36 (1989): 388-390.### Incompleteness and the Philosophy of Mathematics* Boolos, George. "On “Seeing” the Truth of the Gödel Sentence." Behavioral and Brain Sciences 13.4 (1990): 655-656.* [Hilbert’s Program (Stanford Encyclopedia of Philosophy)](https://plato.stanford.edu/entries/hilbert-program/)