春学期の日程・履修案内については以下のページを参照してください。
授業のサポートページです。 ログインのために必要な情報などは、K-LMSの各授業のページを参照してください。
論理と計算の哲学について、基礎から応用まで現代的な観点から解説する。特に「計算可能性」に関連する論理学的な基礎と哲学的な議論の理解を深めるとともに、哲学的な背景をもつ概念や理論が、コンピュータ・サイエンスから現代の人工知能（AI）まで、どのようにして論理と計算にかかわる分野へと応用されてきたのかを検討することを目的とする。
計算可能性の理論は、1930年代のチャーチ、ゲーデル、チューリングらによる一連の研究に遡る。春学期は、こうした古典的な計算モデルのうち、チャーチによるラムダ計算とゲーデルによる再帰関数論に焦点を当てる。また、計算可能性の形式化にかかわる哲学的論点として、チャーチのテーゼをどのように理解するかを検討し、さらに再帰関数論と結びつきの深いゲーデルの不完全性定理の哲学的な帰結、とりわけゲーデルによる機械論・反機械論をめぐる議論を紹介・検討する。
秋学期は、もう一つの代表的な計算モデルであるチューリング・マシンを中心に取り上げる。また、計算の複雑さやチャーチ＝チューリング・テーゼをめぐる近年の哲学的・論理学的議論を紹介し、関連論文を精読・検討する。さらに、計算の哲学の観点から、認知科学における計算モデルについても検討する。履修者の関心に応じて最新の文献も取り上げ、議論を行う。
本講義では非古典論理の立場から現代論理学における諸問題を考察する。本講義の主たる目的は、非古典論理の代数的証明論 (algebraic proof theory) の初歩を習得し、さらに現代論理学の最前線へ哲学的にアプローチするための手法や視点を養うことである。
Gerhard Gentzenが1935年に導入したシークエント計算 (sequent calculus) の存在意義は、彼が発見した「基本定理」 (Hauptsatz)、すなわち、「シークエント計算上のあらゆる導出はカット規則の適用を含まないようなものへと変形可能である」という定理の比類なき重要性により裏付けられている。シークエント計算に対して新たな公理図式を始式として加えるとより強力な論理体系を得ることが可能だが、多くの場合カット除去の破綻という代償を伴う。公理図式の代わりにそれと等価な「良い」推論規則を加えてやることでカット除去が維持されることも経験的には知られてきたが、そうした推論規則の発見は時として論理学者による職人芸に強く依存する。
こうした状況を踏まえ、Ciabattoni, Galatos, and Terui (2008, 2012) が提案した代数的証明論の枠組みの中で「良い」構造規則を得るための系統的方法を学習する。今学期の目標は主に三つである。第一の目標は、彼らの仕事の核心をなす部分構造階層 (substructural hierarchy) の設計思想の把握である。第二の目標は、部分構造階層の非常に低いレイヤーに属する論理的公理が与えられたとき、それと等価でしかもカット除去可能性を保存するような「良い」構造規則群を出力するアルゴリズムを理解することである。さらに第三の目標として、以上を踏まえて、(1) ある対象が「論理」と呼ぶにふさわしいのはそれがどんな性質を満たすときか？ (2) よい（よくない）論理とは何か？ などといった哲学的問題を検討する。