論計祭 # 5「解説！『自然演繹100本ノック』

論計祭 (ろんけいさい) について

今回の論計祭では、『自然演繹100本ノック』を作成者みずから解説します。

論計舎が提供する論計祭は、数理論理学・理論計算機科学を中心としつつも、コンピューターサイエンス・哲学・言語学・法学など様々な意味での 「論と計の科学」 に興味を持った方々に発表の機会を提供するとともに論計舎内外の講師講演を行う場です。

また論と計の科学に関する質問や論計舎のサービスに関する相談にお答えする質問・相談会も含まれます

スピーカー

川井 新 (Shin Quawai)

論計舎主催・講師。 論理と計算の関わりに関心をもち、在野研究者として活躍中。他に哲学的論理学も専門とする。RIMS共同研究にて口頭発表2回。論理学友の会発起人。指導実績のある分野に、線形代数、微分積分学、数理論理学。ウィスキーと珈琲を好む。

『自然演繹100本ノック』について

『自然演繹100本ノック』は論計舎のオリジナル教材です。

この教材では自然演繹の証明図を書く問題を100題提出します。
しかし、数理論理学は、証明図を書く学問ではありません。
では、なぜ100題ノックを世に出すのかという問いは自然なものです。
その答えは、証明図を書くことに脳のリソースを使わないでいいことで、
証明図・証明とは何かを概念的に思考する余裕が生じると考えたからです。

教材へのlink

講演詳細

証明図の書き方の解説を行います。
当教材では、考えないことを強調していますが、
そのために証明図の書き方の解説を行い、
目の前で実際に書いてみようというものです。

1. 証明の形式化の意義、数理論理学とは何か。

2. 自然演繹の紹介。

3. 自然演繹の証明図の書き方。

4. 証明練習 (参加者の方にやってもらいます) 。

「論と計の科学」

論理的に考えるとき、
私たちは step by step でつまり一つ一つの正しい手続きを踏んで結論に至ります。
同様に簡単な計算をするときでも、
私たちは一行ごとに式を変形しながらやはり正しい手続きに従って値を求めます。

実はこの論理と計算が数学的に同じものであるという原理があり、
それをCurry-Howard対応というのですが、
コンピュータという論理的な推論の主役と
プログラミングという計算の世界の王は表裏一体であると考えられています。
このことから、
論計舎は「論と計の科学」を掲げるのです。

論計祭が、そして論計舎が、提供する「論と計の科学」は、
プログラミングはできているけどいっそう複雑だったり大規模だったりするプログラミング業務へ飛躍したい方や
逆にプログラミングをできるようになりたいのにどこから手をつけていいかわからない方の、
ボトルネックを解消するものです。

さらに「論と計」のうち「論」のほうに着目すると、
人間の思考や科学という営みを説明するために哲学であったり、
ことばを話せるとはどういうことかを理解するために言語学であったり、
法律にまつわる厳密な議論を数学的に扱うためだったり、
学術的な世界で様々に使われています。
しかも、それらを産業や実務で応用していこうという動きも盛んになりつつあると言える現状があるでしょう。
したがって、
もしあなたが「正しさ」とか「厳密さ」とかそうしたある種の絶対的な保障や理解を求めるのであれば、
「論と計の科学」はあなたに多くを与えるものなのです。

論計舎は「論と計の科学」を広めることをミッションとし、
その普及を通して世の中を滑らかにそして明らかにすることを願っています。

開催日時

8/24 (土) 16時から18時半まで

タイムテーブル

15:50 開場

16:00 開会と論計舎の紹介

16:15 講師講演「解説！『自然演繹100本ノック』」(60分)

17:15 証明練習

17:45 質疑応答

18:00 論計舎からの案内と質問相談会

18:30 閉会

参加

このページより参加登録いただきますと、 当日開場時にconnpassより会場の詳細がメールにて届きます。

connpass運営からのメールを受信できるように設定しておいてください。

また参加のための情報はconnpass内「参加者への情報」からもご覧になれます。

募集

リスナー

途中の入退室は自由ですので、お気軽にご参加ください。

質問・相談会について

数理論理学および理論計算機科学に関する質問や論計舎のサービスに関する相談を受け付けます。

質問・相談の時間帯では論と計の科学の内容的に踏み込んだ部分から「数理論理学・計算機科学ってなに/どう学んだらいいのか」といった全体的なものまで質問を受け付けるとともに論計舎の受講に関する様々な質問・相談も募集しております。