数理論理学A

前期火2, 共北32


今年度は教室の試験定員までの授業登録者数制限を余儀なくされた関係で、 希望者多数の場合に抽選となってしまうことを御赦し願えればと思います。 もしそうなった場合、4/23頃の登録見直しの際に空きが出れば、 先着順で追加登録が可能となる見込みです。

2021年度のフィードバックの予定は追ってお知らせいたします。

授業の概要・目的

数理論理学は論理を記号化して数学的手法で扱い,数学の基礎や論理構造を研究する分野であり,計算機科学や言語学などにも応用されている.分野としては証明論、モデル論、公理的集合論、計算論に分けられる。記号論理学で扱う様々な論理体系のうち,最も基本的な古典論理(命題論理と一階述語論理)に焦点を絞り,真理値による意味論と公理・推論規則による形式化を解説する.また計算可能な関数を定義し,論理式が真であることの決定可能性について序論的な部分を論じる.証明論とモデル論、計算論の入り口の部分を紹介することとなる。

到達目標

命題論理と一階述語論理についての基本的な概念や考え方、計算の数学的な定義の基本を十分に理解するとともに,具体的な論理式の真偽を判定する方法や証明を組み立てる方法を習得する.

授業計画と内容

予定では,以下の各項目について,項目ごとに0.5~2週の講義を行う.但し進度等の事情により一部を省略する場合がある.授業の最初に前回についての演習問題を解く場合がある。

1. 数理論理学とは何か:問題意識、発展の歴史,関連する分野,参考文献

2. 命題論理の考え方:原子命題と論理結合子,論理式,真理値,論理演算,真理値表

3. 判定するということ:決定可能性,計算可能な関数の定義,計算不可能な関数の存在

4. 命題論理の恒真式,同値な式,さまざまな例

5. 論理式の標準形:論理積標準形と論理和標準形,標準形への同値変形,恒真性や充足可能性との関係

6. 形式化の考え方:形式的推論,公理と推論規則,形式的体系の例,完全性と健全性

7. 命題論理式の決定可能性:決定手続き,SAT問題,NP完全問題

8. シーケント計算による命題論理の形式化:論理式の構成,論理結合子に関する導入と除去の規則,形式的推論のさまざまな例

9. 述語論理の考え方:述語,対象変数,量化子,論理式の構成,論理式の意味,数学的主張を論理式に翻訳すること

10. 述語論理の意味論的概念:意味解釈の枠組,恒真式,同値な式,さまざまな例,冠頭標準形

11. 述語論理の形式化:量化子に関する推論規則,固有変数条件,形式的推論のさまざまな例

12. 理論の論理的記述:理論とモデル,等号公理,ペアノ算術の公理,論理プログラミング

13. 述語論理の完全性定理:健全性と完全性,完全性定理のさまざまな定式化,完全性定理の証明

14. 述語論理の決定可能性

関連する授業

数理論理学B(後期火2) この講義の続き。計算可能性など。

プログラミング演習(LISP)(前期水4,5) 記号処理プログラミングの基本を学ぶ。

関連する授業(総合人間学部学部主催の情報関係の授業)

数理科学特論III(総合人間学部学部科目、後期集中) 記号的AIと統計的AIの融合