Math 342, Set theory and Logic, Spring 2023

Instructor: Jun Li T Th 11:00am -12:30, 300 Science Center

Office Hour: T W Th 12:30pm -2:00pm, or by appointment, 329G Science Center.

Syllabus: S23_342_syllabus. More information on Isidore.

Main reference: [Glynn Winskel] Set theory for computer science, notes from Cambridge.
[Krzysztof Ciesielski] Set Theory for the Working Mathematician.
The first half of the course will cover basics like axioms and properties of sets, Cantor's theorem, real number axioms, and model theory.
The second half will focus on Godel Incompleteness Theorem. The final goal is to provide a precise statement and rigors proofs. Along the way, we will talk about three computability models, i.e. Godel's general recursive sets, Church's lambda calculus and Turing machine. We'll make use of those in a project on Lean math prover.

Meeting Topic Lecture notes
1 Overview
Course content and semester goal. 		Overview
2 Set Operations SetOperations.pdf
3 Logic logic.pdf
4 Model Theory ModelTheory.pdf
5 Functions and Relations FunctionsRelations.pdf
6 Cantor's Theorem Cantor'sTheorem.pdf
7 Real Number Axioms RealNuberAxioms.pdf
8 Lambda Calculus LambdaCalculus.pdf
9 Induction Induction.pdf
10 Interactive Proof InteractiveProof.pdf
11 Tarski's Fixed-Point Theorem TarskiFixedPointTheorem.pdf
12 Well-Founded Induction WellFoundedInduction.pdf
13 Computability vs. Diagonal Argument Computability_VS_DiagonalArgument.pdf
14 Type Theory TypeTheory.pdf
15 Lean Lean Math Prover, a tutorial
16 Stander Poster Lean Math Library
17 Stander Poster More Lean with Kevin Buzzard
18 Towards Incompleteness Theorem Toward_Incompleteness_Theorem.pdf
19 Gödel's Incompleteness Proof Godel_Incompleteness_proof.pdf
20 Gödel's Proof II GodelProofII.pdf