Fixpoints and Induction in Logic and Computer Science
Lecture in the summer term 2022
This course is about the proof method of induction, and about the theory of fixpoints on ordered structures, complete lattices in particular. Topics covered are:
- Induction on natural numbers, structural induction, well-founded induction
- Tarski's fixpoint theorem for monotonic functions on complete lattices and variations on complete partial orders
- Examples from games, probability theory (Markov chains and decision processes), program semantics and verification, automata theory and formal languages
- Computation of fixpoints by iteration on finite lattices
- Characterization of fixpoints on infinite lattices for continuous functions and arbitrary functions
- Ordinal numbers, transfinite induction, well-ordering theorem
- First-order logic with fixpoints
- The role of induction in incompleteness theorem for Peano arithmetic
It is assumed that students are familiar with basics in discrete mathematics, automata theory, computability, and mathematical logic, as taught in the corresponding bachelor courses in computer science at RWTH Aachen.
Time and Places
It is planned ot have oral exams for the course. Depending on the number of students it might also be a written exam.