Content under update
Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20-17:50 (Beijing), Monday, 2026-03-02 ~ 2026-04-20
Venue: A3-2-301, BIMSA
Online: Zoom: 787 662 9899 PW: BIMSA
Wechat group and more: https://www.bimsa.net/activity/LogandComIII/
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 02 Mar (Mon) | Fundamentals of computation [LCIII-00-01] | video00-01 | |
| 2 | 09 Mar (Mon) | Fundamentals of math logic [LCIII-00-02] | video00-02 | |
| 3 | 16 Mar (Mon) | Oracle computation and relativized arithmetical hierarchy [LCIII-0101] | video01-01 | |
| 4 | 23 Mar (Mon) | Analytical hierarchy, ordinals and well-founded trees [LCIII-0102] | video01-02 | |
| 5 | 30 Mar (Mon) | Constructive ordinals and Kondo’s theorem [LCIII-0103] | video01-03 | |
| 6 | 13 Apr (Mon) | KP set theory I [LCIII-0201] | video02-01 | |
| 7 | 20 Apr (Wen) | KP set theory II [LCIII-0202] | video02-02 |
Content under update
Lecturer: Kazuyuki Tanaka
Lecture Time: 15:20-17:50 (Beijing), Monday, 2025-09-17 ~ 2025-12-10
Venue: 六教B 403, 清华大学 Tsinghua University
Part 1. Equational theory
Part 2. First order theory
Part 3. Basic Model theory
Part 4. First order arithmetic and incompleteness theorems
Part 5. Models of first-order arithmetic
Part 6. Reverse mathematics
Part 7. Second order arithmetic and non-standard methods
| No. | Date | Slides | Recordings | Further readings |
|---|---|---|---|---|
| 1 | 17 Sep (Wen) | Formal systems of equations [FM01-01] | video01-01 | |
| 2 | 19 Sep (Fri) | Birkhoff’s theorems and Boolean algebras [FM01-02] | video01-02 | |
| 3 | 24 Sep (Wen) | Boolean algebras (continued) and propositional logic [FM01-03] | video01-03 | |
| 4 | 26 Sep (Fri) | Computable functions and general recursive functions [FM01-04] | video01-04 | |
| 5 | 10 Oct (Fri) | First order logic: formal systems and structures [FM02-01] | video02-01 | |
| 6 | 11 Oct (Sat) | Goedel completeness theorem and applications [FM02-02] | video02-02 | |
| 7 | 15 Oct (Wen) | Various forms of axiomatic systems [FM03-01] | video03-01 | |
| 8 | 17 Oct (Fri) | Horn theory and reduced products [FM03-02] | video03-02 | |
| 9 | 22 Oct (Wen) | Ultra products and non-standard analysis [FM03-03] | video03-03 | |
| 10 | 24 Oct (Fri) | Peano arithmetic and representation theorems [FM04-01] | video04-01 | |
| 11 | 29 Oct (Wen) | The first incompleteness theorem [FM04-02] | video04-02 | |
| 12 | 31 Oct (Fri) | The second incompleteness theorem [FM04-03] | video04-03 | 13 | 05 Nov (Wen) | Nonstandard models and Overspill [FM05-00] | video05-00 |
| 14 | 07 Nov (Fri) | The omitting type theorem [FM05-01] | video05-01 | 15 | 12 Nov (Wen) | Recursively saturated models [FM05-02] | video05-02 |
| 16 | 14 Nov (Fri) | Friedman’s theorem [FM05-03] | video05-03 | |
| 17 | 19 Nov (Wen) | Resplendency [FM05-04] | video05-04 | |
| 18 | 21 Nov (Fri) | Real numbers in RCA_0 [FM06-01and02] | video06-01and02 | 19 | 26 Nov (Wen) | Completeness of the reals and ACA_0 [FM06-03] | video06-03 |
| 20 | 28 Nov (Fri) | Continuous functions and WKL_0 [FM06-04] | video06-04 | |
| 21 | 3 Dec (Wen) | A self-embedding theorem I [FM07-01] | video06-01 | |
| 22 | 5 Dec (Fri) | A self-embedding thm II and Harrington’s conservation thm [FM07-02] | video07-02 | 23 | 10 Dec (Wen) | STY theorem [FM07-03] | video07-03 |
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 (Thu) | Kripke completeness [LC04-02] | video04-02 | |
| 3 | 11 Mar (Tue) | Standard translation and bisimulation [LC04-03] | video04-03 | |
| 4 | 13 Mar (Thu) | Decision problem [LC04-04] | video04-04 | |
| 5 | 18 Mar (Tue) | Computational complexity [LC04-05] | video04-05 | |
| 6 | 20 Mar (Thu) | Multi-modal and predicate logics [LC04-06] | video04-06 | |
| 7 | 25 Mar (Tue) | Modal predicate logics and epistemic logic [LC04-07] | video04-07 | |
| 8 | 27 Mar (Thu) | Introduction to modal $\mu$-calculus and monadic second-order logic [LC05-01] | video05-01 | |
| 9 | 01 Apr (Tue) | Basics of modal $\mu$-calculus [LC05-02] | video05-02 | |
| 10 | 03 Apr (Thu) | The adequacy theorem [LC05-03] | video05-03 | |
| 11 | 08 Apr (Tue) | CTL [LC05-04] | video05-04 | |
| 12 | 10 Apr (Thu) | Applications [LC05-05] | video05-05 | |
| 13 | 15 Apr (Tue) | Second-order arithmetic and analytical hierarchy [LC06-01] | video06-01 | |
| 14 | 17 Apr (Thu) | Buechi automata [LC06-02] | video06-02 | |
| 15 | 22 Apr (Tue) | Safra’s theorem [LC06-03] | video06-03 | |
| 16 | 24 Apr (Thu) | The decidability of S1S [LC06-04] | video06-04 | |
| 17 | 6 May (Tue) | Tree automata [LC06-05] | video06-05 | |
| 18 | 8 May (Thu) | Tree automata and parity games [LC06-06] | video06-06 | |
| 19 | 13 May (Tue) | The decidability of S2S [LC06-07] | video06-07 | |
| 20 | 15 May (Thu) | Positional determinacy of parity games [LC06-08] | video06-08 | |
| 21 | 20 May (Tue) | Oracle computation and relativization [LC07-01] | video07-01 | |
| 22 | 22 May (Thu) | m-reducibility and simple sets [LC07-02] | video07-02 | |
| 23 | 27 May (Tue) | T-reducibility and Post’s problem [LC07-03] | video07-03 | |
| 24 | 29 May (Thu) | Miscellaneous [LC07-04] | video07-04 |
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 these courses?
K. Tanaka, 計算理論と数理論理学 (Mathematics of Logic and Computation, in Japanese), 共立出版 2022.
K. Tanaka, 数学基礎論序説 －数の体系への論理的アプローチ－ (Logical Foundations of Mathematics: A Logical Approach to Number Systems, in Japanese), 裳華房 2019.
H.D. Ebbinghaus, H. Flum and W. Thomas, Mathematical Logic, 3rd ed., Springer 2021.
D.C. Kozen, Theory of Computation, Springer 2006.
Workshop on Logic and Computation (迷你-CTFM), BIMSA, Beijing, 2025
BIMSA Workshop on Set Theory and Logic, BIMSA, Beijing, 2025
We acknowledge the support from Academic Department of BIMSA, TUHEP and AireLinux.