Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20-16:55 (Beijing), Tuesday and Thursday, 2025-03-04 ~ 2025-05-29
Venue: A3-2-301, BIMSA
Online: Zoom: 230 432 7880 PW: BIMSA
Wechat group and more: https://bimsa.net/activity/LogandComII/
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 04 Mar (Tue) | Kripke models and normal logics [LC04-01] | video04-01 | |
| 2 | 06 Mar (Tue) | Kripke completeness [LC04-02] | video04-02 |
Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20-16:55 (Beijing), Tuesday and Thursday, 2024-09-10 ~ 2024-12-19
Venue: A3-2-301, BIMSA
Online: Zoom: 787 662 9899 PW: BIMSA
Wechat group and more: https://bimsa.net/activity/LogandComI/
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 10 Sep (Tue) | Automata and monoids [LC01-01] | video01-01 | [hopcroft_CHI] [hopcroft_ENG] |
| 2 | 12 Sep (Thu) | Turing machines [LC01-02] | video01-02 | |
| 17 Sep (Tue) | holiday | |||
| 3 | 19 Sep (Thu) | Computable functions and primitive recursive functions [LC01-03] | video01-03 | |
| 4 | 24 Sep (Tue) | Decidability and undecidability [LC01-04] | video01-04 | [N. Cutland(1980)] |
| 5 | 26 Sep (Thu) | Partial recursive functions and computable enumerable sets [LC01-05] | video01-05 | |
| 01 Oct(Tue) | holiday | |||
| 03 Oct (Thu) | holiday | |||
| 6 | 08 Oct (Tue) | Rice's theorem and many-one reducibility [LC01-06] | video01-06 | |
| 7 | 10 Oct (Thu) | Tautologies and proofs [LC02-01] | video02-01 | |
| 8 | 15 Oct (Tue) | The completeness theorem of propositional logic [LC02-02] | video02-02 | |
| 9 | 17 Oct (Thu) | SAT and NP-complete problems [LC02-03] | video02-03 | |
| 10 | 22 Oct (Tue) | NP-complete problems about graph [LC02-04] | video02-04 | |
| 11 | 24 Oct (Thu) | Time-bound and space-bound complexity classes [LC02-05] | video02-05 | |
| 12 | 29 Oct (Tue) | Relations between Time and space complexity classes [LC02-06] | video02-06 | |
| 13 | 31 Oct (Thu) | Hierarchy theorems,PSPACE-completeness and TQBF [LC02-07] | video02-07 | |
| 14 | 5 Nov (Tue) | What is first-order logic? [LC03-01] | video03-01 | |
| 15 | 7 Nov (Thu) | Skolem's theorem[LC03-02] | video03-02 | |
| 16 | 12 Nov (Tue) | Gödel's completeness theorem[LC03-03] | video03-03 | |
| 17 | 14 Nov (Thu) | Ehrenfeucht-Fraïssé's theorem I[LC03-04] | video03-04 | |
| 18 | 19 Nov (Tue) | Ehrenfeucht-Fraïssé's theorem II[LC03-05] | video03-05 | |
| 19 | 21 Nov (Thu) | Presburger arithmetic[LC03-06] | video03-06 | |
| 20 | 26 Nov (Tue) | Peano arithmetic[LC03-07] | video03-07 | |
| 21 | 28 Nov (Thu) | Gödel's first incompleteness theorem[LC03-08] | video03-08 | |
| 22 | 3 Dec (Thu) | Gödel's second incompleteness theorem[LC03-09] | video03-09 | 23 | 5 Dec (Tue) | Second order logic[LC03-10] | video03-10 | 24 | 10 Dec (Thu) | Second order arithmetic[LC03-11] | video03-11 |
| No. | Homeworks | Submission | Due date |
|---|---|---|---|
| 1 | Quiz 1 | [Quiz 1] | 2024-09-26 |
| 2 | Exercise0103 [exe0103-pdf] [exe0103-TEX] | liwj(AT)bimsa.cn | |
| 3 | Exercise0104 [exe0104-pdf] [exe0104-TEX] | liwj(AT)bimsa.cn | |
| 4 | Exercise0105 [exe0105-pdf] [exe0105-TEX] | liwj(AT)bimsa.cn | |
| 5 | Exercise0106 [exe0106-pdf] [exe0106-TEX] | liwj(AT)bimsa.cn | |
| 6 | Exercise0201 [exe0201-pdf] [exe0201-TEX] | liwj(AT)bimsa.cn | |
| 7 | Exercise0202 [exe0202-pdf] [exe0202-TEX] | liwj(AT)bimsa.cn | |
| 8 | Exercise0203 [exe0203-pdf] [exe0203-TEX] | liwj(AT)bimsa.cn | |
| 9 | Exercise0204 [exe0204-pdf] [exe0204-TEX] | liwj(AT)bimsa.cn | |
| 10 | Exercise0205 [exe0205-pdf] [exe0205-TEX] | liwj(AT)bimsa.cn | |
| 11 | Exercise0206 [exe0206-pdf] [exe0206-TEX] | liwj(AT)bimsa.cn | |
| 12 | Exercise0207 [exe0207-pdf] [exe0207-TEX] | liwj(AT)bimsa.cn | |
| 13 | Exercise0302 [exe0302-pdf] [exe0302-TEX] | liwj(AT)bimsa.cn |
Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20-16:55 (Beijing), Tuesday and Thursday, 2024-03-12 ~ 2024-06-13
Venue: A3-2-301, BIMSA
Online: Zoom: 559 700 6085 PW: BIMSA
Wechat group and more: https://bimsa.net:10000/activity/LogandFouII/
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 12 Mar (Tue) | Reviews [lec05_03] | [video05-03] | |
| 2 | 14 Mar (Thu) | Friedman’s theorem [lec05_04] | [video05-04] | |
| 3 | 19 Mar (Tue) | Friedman’s theorem (continued) and introduction to resplendency [lec05_05] | [video05-05] | |
| 4 | 21 Mar (Thu) | Resplendency and applications [lec05_06] | [video05-06] | |
| 5 | 26 Mar (Tue) | Resplendency and applications (continued) [lec05_07] | [video05-07] | |
| 6 | 28 Mar (Thu) | Basic properties of one-variable polynomial [lec06_01] | [video06-01] | |
| 7 | 02 Apr (Tue) | Real closed ordered fields and the Artin-Schreier theorem [lec06_02] | [video06-02] | |
| 8 | 09 Apr (Tue) | Quantifier elimination of RCOF [lec06_03] | [video06-03] | |
| 9 | 11 Apr (Thu) | Hilbert’s 17th problem and o-minimal theories [lec06_04] | [video06-04] | |
| 10 | 16 Apr (Tue) | Introduction and the base system RCA0 [lec07_01] | [video07-01] | |
| 11 | 18 Apr (Thu) | Defining real numbers in RCA0 [lec07_02] | [video07-02] | |
| 12 | 23 Apr (Tue) | Completeness of the reals and ACA0 [lec07_03] | [video07-03] | |
| 13 | 25 Apr (Thu) | Continuous functions and WKL0 [lec07_04] | [video07-04] | |
| 14 | 30 Apr (Tue) | Continuous functions and WKL0, II [lec07_05] | [video07-05] | |
| 15 | 09 May (Thu) | Koenig’s lemma and Ramsey’s theorem [lec07_06] | [video07-06] | |
| 16 | 14 May (Tue) | Determinacy of infinite games I [lec07_07] | [video07-07] | |
| 17 | 16 May (Thu) | Determinacy of infinite games II [lec07_08] | [video07-08] | |
| 18 | 21 May (Tue) | Determinacy of infinite games III + Introduction to forcing [lec07_09] | [video07-09] | |
| 19 | 23 May (Thu) | Harrington’s conservation result on WKL0 [lec08_01] | [video08-01] | |
| 20 | 28 May (Tue) | Harrington’s conservation result on WKL0 II [lec08_01] | [video08-02] | |
| 21 | 30 May (Thu) | Harrington’s conservation result on WKL0 III and a self-embedding theorem I [lec08_03] | [video08-03] | |
| 22 | 04 June (Tue) | A self-embedding theorem II [lec08_04] | [video08-04] | |
| 23 | 06 June (Thu) | A self-embedding theorem III and STY theorem I [lec08_05] | [video08-05] | |
| 24 | 11 June (Tue) | STY theorem II [lec08_06] | [video08-06] |
Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20 ~ 17:50 (Beijing), Thursday, 2023-09-21 ~ 2024-01-11
Venue: YMSC-B725
Online: Zoom: 482 240 1589 PW: BIMSA
Wechat group and more: https://bimsa.net/activity/logicfoundationsI/
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 21 Sep (Thu) | Formal systems of equation [lec01_01] | [video01-01] | |
| 2 | 28 Sep (Thu) | Free algebras and Birkhoff’s theorem [lec01_02] | [video01-02] | |
| 3 | 12 Oct (Thu) | Boolean algebras [lec01_03] | [video01-03] | |
| 4 | 19 Oct (Thu) | Computable functions and general recursive function [lec01_04] | [video01-04] | |
| 5 | 26 Oct (Thu) | First order logic: formal system GT and structures [lec02_01] | [video02-01] | |
| 6 | 02 Nov (Thu) | Goedel completeness theorem and applications [lec02_02] | [video02-02] | |
| 7 | 09 Nov (Thu) | Miscellaneous [lec02_03] | [video02-03] | |
| 8 | 16 Nov (Thu) | $\forall$-theory and $\forall \exists$-theory [lec03-01] | [video03-01] | |
| 9 | 23 Nov (Thu) | Horn theory and reduced products [lec03-02] | [video03-02] | |
| 10 | 30 Nov (Thu) | Ultra products and non-standard analysis [lec03-03] | [video03-03] | |
| 11 | 07 Dec (Thu) | Peano arithmetic and representation theorems [lec04-01] | [video04-01] | |
| 12 | 14 Dec (Thu) | The first incompleteness theorem [lec04-02] | [video04-02] | |
| 13 | 21 Dec (Thu) | The second incompleteness theorem [lec04-03] | [video04-03] | |
| 14 | 28 Dec (Thu) | Presburger arithmetic [lec04-04] | [video04-04] | |
| 15 | 04 Jan (Thu) | Non-standard models and the omitting type theorem [lec05-01] | [video05-01] | |
| 16 | 11 Jan (Thu) | Recursively saturated models [lec05-02] | [video05-02] |
| No. | Homeworks | Submission | Due date |
|---|---|---|---|
| 1 | Homework 1 [hw1-pdf] [hw1-TEX] | logic+hw1(AT)airelinux[dot]org | 2023-09-25 |
| 2 | Homework 2 [hw2-pdf] [hw2-TEX] | logic+hw2(AT)airelinux[dot]org | 2023-10-09 |
| 3 | Homework 3 [hw3-pdf] [hw3-TEX] | logic+hw3(AT)airelinux[dot]org | 2023-10-18 |
| 4 | Homework 4 [hw4-pdf] [hw4-TEX] | logic+hw4(AT)airelinux[dot]org | 2023-10-22 |
| 5 | Homework 5 [hw5-pdf] [hw5-TEX] | logic+hw5(AT)airelinux[dot]org | 2023-11-01 |
| 6 | Homework 6 [hw6-pdf] [hw6-TEX] | logic+hw6(AT)airelinux[dot]org | 2023-11-07 |
| 7 | Homework 7 [hw7-pdf] [hw7-TEX] | logic+hw7(AT)airelinux[dot]org | 2023-11-15 |
| 8 | Homework 8 [hw8-pdf] [hw8-TEX] | logic+hw8(AT)airelinux[dot]org | 2023-11-20 |
| 9 | Homework 9 [hw9-pdf] [hw9-TEX] | logic+hw9(AT)airelinux[dot]org | 2023-11-28 |
| 10 | Homework 10 [hw10-pdf] [hw10-TEX] | logic+hw10(AT)airelinux[dot]org | 2023-12-06 |
| 11 | Homework 11 [hw11-pdf] [hw11-TEX] | logic+hw11(AT)airelinux[dot]org | |
| 12 | Homework 12 [hw12-pdf] [hw12-TEX] | logic+hw12(AT)airelinux[dot]org | 2023-12-19 |
| 13 | Homework 13 [hw13-pdf] [hw13-TEX] | logic+hw13(AT)airelinux[dot]org | 2024-01-04 |
| 14 | Homework 14 [hw14-pdf] [hw14-TEX] | logic+hw14(AT)airelinux[dot]org |
Lecturer: Kazuyuki Tanaka
Lecture Time: 10:40 - 12:15 (Beijing), Tuesday and Thursday, 07 March to 06 June, 2023
Venue: 1108, BIMSA
Online: Zoom: 293 812 9202 PW: BIMSA
13 April, 2023: There will be no class on April 18 and 20, 2023.
Before Golden Week, we still have two classes on April 25 and 27, 2023.
11 April, 2023: Please scan the following QR code to join our questionnaire.
Or, you can go to questionnaire.
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 07 March (Tue) | First-order logic [lecture04_01] | [video04-01] | |
| 2 | 09 March (Thu) | Arithmetical formulas [lecture04_02] | [video04-02] | |
| 3 | 14 March (Tue) | Gödel’s first incompleteness theorem [lecture04_03] | [video04-03] | |
| 4 | 16 March (Thu) | Gödel’s second incompleteness theorem [lecture04_04] | [video04-04] | [Goedel Without (Too Many) Tears] |
| 5 | 21 March (Tue) | Second-order logic [lecture04_05] | [video04-05] | |
| 6 | 23 March (Thu) | Analytical formulas [lecture04_06] | [video04-06] | |
| 7 | 28 March (Tue) | Automata on infinite strings [lecture05_01] | [video05-01] | |
| 8 | 30 March (Thu) | ω-automata and S1S [lecture05_02] | [video05-02] | |
| 9 | 4 April (Tue) | Tree automata and S2S (1) [lecture05_03] | [video05-03] | |
| 10 | 6 April (Thu) | Tree automata and S2S (2) [lecture05_04] | [video05-04] | |
| 11 | 11 April (Tue) | Finite model theory [lecture05_05] | [video05-05] | |
| 12 | 13 April (Thu) | Parity games [lecture05_06] | [video05-06] | |
| 13 | 25 April (Tue) | Oracle computation and relativization [lecture06-01] | [video06-01] | |
| 14 | 27 April (Thu) | m-reducibility and simple sets [lecture06-02] | [video06-02] | |
| 15 | 4 May (Thu) | T-reducibility and Post’s problem [lecture06-03] | [video06-03] | |
| 16 | 9 May (Tue) | Arithmetical hierarchy and polynomial-time hierarchy [lecture06-04] | [video06-04] | |
| 17 | 11 May (Thu) | Analytical hierarchy and descriptive set theory I [lecture06-05] | [video06-05] | |
| 18 | 16 May (Tue) | Analytical hierarchy and descriptive set theory II [lecture06-06] | [video06-06] | |
| 19 | 18 May (Thu) | KP set theory I [lecture07-01] | [video07-01] | |
| 20 | 23 May (Tue) | KP set theory II [lecture07-02] | [video07-02] | |
| 21 | 25 May (Thu) | KP set theory III [lecture07-03] | [video07-03] | |
| 22 | 30 May (Tue) | KP set theory IV and $\alpha$ recursion theory I [lecture07-04] | [video07-04] | |
| 23 | 1 June (Thu) | Recursively large ordinals I [lecture07-05] | [video07-05] | |
| 24 | 6 June (Thu) | Recursively large ordinals II and second order arithmetic [lecture07-06] | [video07-06] |
| No. | Homeworks | Submission | Due date |
|---|---|---|---|
| 11 | Homework 11 [hw11-pdf] [hw11-TEX] | logic+hw11(AT)airelinux[dot]org | |
| 12 | Homework 12 [hw12-pdf] [hw12-TEX] | logic+hw12(AT)airelinux[dot]org | 29 March 2023, 11:59 pm (Beijing) |
| 13 | Homework 13 [hw13-pdf] [hw13-TEX] | logic+hw13(AT)airelinux[dot]org | 03 April 2023, 11:59 pm (Beijing) |
| 14 | Homework 14 [hw14-pdf] [hw14-TEX] [hwbonus1-pdf] [hwbonus1-TEX] | logic+hw14(AT)airelinux[dot]org | 10 April 2023, 11:59 pm (Beijing) |
| 15 | Homework 15 [hw15-pdf] [hw15-TEX] | logic+hw15(AT)airelinux[dot]org | 17 April 2023, 11:59 pm (Beijing) |
| 16 | Homework 16 [hw16-pdf] [hw16-TEX] | logic+hw16(AT)airelinux[dot]org | 4 May 2023, 11:59 pm (Beijing) |
Lecturer: Kazuyuki Tanaka
Lecture Time: 10:40 - 12:15 (Beijing), Tuesday and Thursday, 27 October to 27 December, 2022
Venue: 1110, BIMSA
Online: Zoom: 928 682 9093 PW: BIMSA
03 November, 2022: We encourage everyone to sumbit homework (or partial of homework) and
participate the quiz in class, which is helpful to evaluate your understanding of the lecture and
provide us valuable feedback to improve the class.
Late submission of homework is acceptable, but make sure you can catch up with the lecture.
27 October, 2022: Please scan the following QR code to join our questionnaire.
Alternatively, you can click questionnaire.
Homework will be posted weekly. Please find more in *Homeworks*.
For short questions during the class, please send them to TA via zoom chat.
If you have long questions, we encourage you send them to logic+quest(AT)airelinux[dot]org.
Some frequently asked questions will be posted in *FAQ* with answers.
We will have short Q&A or feedback on homeworks at the end of each lecture.
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 27 October (Thu) | Introduction, automata and monoid [lecture01-01] | [video01-01] | |
| 2 | 01 November (Tue) | Turing machines [lecture01-02] | [video01-02] | |
| 3 | 03 November (Thu) | Computable functions and primitive recursive functions [lecture01-03] | [video01-03] | [N. Cutland(1980)] |
| 4 | 08 November (Tue) | Decidability and undecidability [lecture01-04] | [video01-04] | |
| 5 | 10 November (Thu) | Partial recursive functions and computable enumerable sets [lecture01-05] | [video01-05] | |
| 6 | 15 November (Tue) | Rice's theorem and many-one reducibility [lecture01-06] | [video01-06] | [H. Rogers(1967)] |
| 7 | 17 November (Thu) | Tautologies and proofs [lecture02-01] | [video02-01] | Chapter 1 of [E. Mendelson(2015)] |
| 8 | 22 November (Tue) | The completeness theorem of propositional logic [lecture02-02] | [video02-02] | |
| 9 | 24 November (Thu) | SAT and NP-complete problems [lecture02-03] | [video02-03] | [M. Sipser(2012)] |
| 10 | 29 November (Tue) | NP-complete problems about graph [lecture02-04] | [video02-04] | |
| 11 | 01 December (Thu) | Time-bound and space-bound complexity classes [lecture02-05] | [video02-05] | [D.C. Kozen(2006)] |
| 12 | 06 December (Tue) | PSPACE-completeness and TQBF [lecture02-06] | [video02-06] | |
| 13 | 08 December (Thu) | What is first-order logic? [lecture03-01] | [video03-01] | (1).[The Emergence of FO] (2).[List of FO theories] OR [pdf] |
| 14 | 13 December (Tue) | Skolem's theoremt [lecture03-02] | [video03-02] | |
| 15 | 15 December (Thu) | Gödel's completeness theorem [lecture03-03] | [video03-03] | |
| 16 | 20 December (Tue) | Ehrenfeucht-Fraïssé's theorem [lecture03-04] | [video03-04] | [Logic and Games] |
| 17 | 22 December (Thu) | Presburger arithmetic [lecture03-05] | [video03-05] | |
| 18 | 27 December (Tue) 🏆 | Peano arithmetic and Gödel's first incompleteness theorem [lecture03-06] | [video03-06] |
| No. | Homeworks | Submission | Due date |
|---|---|---|---|
| 1 | Homework 1 [hw1-pdf] [hw1-TEX] [questionnaire] | logic+hw1(AT)airelinux[dot]org | 01 November 11:59 pm (Beijing) |
| 2 | Homework 2 [hw2-pdf] [hw2-TEX] [quiz1] | logic+hw2(AT)airelinux[dot]org | 07 November 11:59 pm (Beijing) |
| 3 | Homework 3 [hw3-pdf] [hw3-TEX] | logic+hw3(AT)airelinux[dot]org | 14 November 11:59 pm (Beijing) |
| 4 | Homework 4 [hw4-pdf] [hw4-TEX] [quiz2] | logic+hw4(AT)airelinux[dot]org | 21 November 11:59 pm (Beijing) |
| 5 | Homework 5 [hw5-pdf] [hw5-TEX] | logic+hw5(AT)airelinux[dot]org | 28 November 11:59 pm (Beijing) |
| 6 | Homework 6 [hw6-pdf] [hw6-TEX] | logic+hw6(AT)airelinux[dot]org | 5 December 11:59 pm (Beijing) |
| 7 | Homework 7 [hw7-pdf] [hw7-TEX] | logic+hw7(AT)airelinux[dot]org | 12 December 11:59 pm (Beijing) |
| 8 | Homework 8 [hw8-pdf] [hw8-TEX] | logic+hw8(AT)airelinux[dot]org | 19 December 11:59 pm (Beijing) |
| 9 | Homework 9 [hw9-pdf] [hw9-TEX] | logic+hw9(AT)airelinux[dot]org | |
| 10 | Homework 10 [hw10-pdf] [hw10-TEX] | logic+hw10(AT)airelinux[dot]org |
Please replace (AT) and [dot] with @ and . in the above email addresses.
What are the reference books of this course?
H.D. Ebbinghaus, H. Flum and W. Thomas, Mathematical Logic, 3rd ed., Springer 2021.
D.C. Kozen, Theory of Computation, Springer 2006.
K. Tanaka, 計算理論と数理論理学 (Mathematics of Logic and Computation, in Japanese), Kyoritsu 2022.
The lecture slides of this course translate almost all the contents of III.
Besides, further readings are provided in the summary of each lecture.
Please refer to Lecture**.pdf --> Summary --> Further readings.
We acknowledge the support from BIMSA, TUHEP and AireLinux.