人文科学研究科Graduate School of Humanities
PHL600B1（哲学 / Philosophy 600）論理学研究Ⅰ－１Study on Logic I - 1
安東 祐希
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 人文科学研究科Graduate School of Humanities |
| 添付ファイル名Attached documents | |
| 年度Year | 2021 |
| 授業コードClass code | X0010 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 春学期授業/Spring |
| 曜日・時限Day/Period | 月2/Mon.2 |
| 科目種別Class Type | |
| キャンパスCampus | 市ヶ谷 |
| 教室名称Classroom name | |
| 配当年次Grade | |
| 単位数Credit(s) | 2 |
| 備考（履修条件等）Notes | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| カテゴリーCategory | 哲学専攻(修士課程)-専門科目 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
This course deals with the proof of Gentzen's Hauptsatz.
授業で使用する言語Default language used in class
日本語・英語併用 / Japanese & English
授業の概要と目的（何を学ぶか）Outline and objectives
ゲンツェンの基本定理の証明を学ぶ。
到達目標Goal
基本定理の証明を細部にわたり理解し、自ら証明を書くことができる。
授業で使用する言語Default language used in class
日本語・英語併用 / Japanese & English
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
［授業形式：対面授業］
原論文の英訳に従い、省略されている詳細部分も含め、証明の内容を履修者が分担して発表し、それに対して教員および参加者により質疑応答を行う。（発表が「課題」であり、質疑応答において「フィードバック」する。）
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
あり / Yes
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
春学期
※各回の授業形態は予定です。教員の指示に従ってください。
第1回：証明の方針
論文(III:3.1前文)部分
第2回：自由変数の付け替え
論文(III:3.10)部分
第3回：左上式が公理
論文(III:3.111-112)部分
第4回：左上式が右弱化
論文(III:3.113.1-2)部分
第5回：上式が左右連言等
論文(III:3.113.31-32)部分
第6回：上式が左右全称等
論文(III:3.113.33-36)部分
第7回：右階数が1より大
論文(III:3.121前文)部分
第8回：Ｉが左構造規則
論文(III:3.121.21)部分
第9回：Ｉの上式が一つ
論文(III:3.121.22)部分
第10回：Ｉの上式が二つ
論文(III:3.121.23)部分
第11回：右階数が1
論文(III:3.122)部分
第12回：NJにおける切断
論文(III:3.21)部分
第13回：階数が2
論文(III:3.231)部分
第14回：階数が2より大
論文(III:3.232)部分
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
論文に書かれた証明の各段階において、具体的な例を考え、証明図を実際に紙に書きながら十分に考察する。
テキスト（教科書）Textbooks
G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift, 39 (1935) の M. E. Szaboによる英訳、Investigations into logical deduction, in The collected papers of Gerhard Gentzen, North-Holland Publishing Company, 1969
参考書References
・Jon Barwise (ed.), Handbook of Mathematical Logic, Elsevier, 1977
・A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory Second Edition, Cambridge University Press, 2000
成績評価の方法と基準Grading criteria
到達目標に関する問題の提示・解題能力を担当箇所の発表内容（60％）において、さらに、目標の問題全般にわたる理解度を他者担当時の質疑応答（40％）において評価する。
学生の意見等からの気づきChanges following student comments
具体例への適用に関してより多くの時間が取れるようにしたい。
担当教員の専門分野等
〈専門領域〉
数理論理学（証明論）
〈研究テーマ〉
証明図の正規化手続きに関する諸性質
〈主要研究業績〉
・Church-Rosser property of a simple reduction for full first-order classical natural deduction, Annals of Pure and Applied Logic 119 (2003) pp225-237, Elsevier.
・A representation of essential reductions in sequent calculus (abstract), The Bulletin of Symbolic Logic 11 (2005) pp265-265, The Association for Symbolic Logic.
・Gentzen's unpublished normalization theorem and its successors, 数理解析研究所講究録 2083『証明論と証明活動』(2018) pp146-149, 京都大学数理解析研究所.