Bonjour,
Monday 26 February, 15:00 at EPITA KB 204 and online (link at https://www.lre.epita.fr/automata_seminars/ when available)
Speaker: Jérémy Dubut-Kross, National Institute of Advanced Science and Technology, Tokyo
Title: Fixed-Point Theorems for Non-Transitive Relations
We develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden. Joint work with Akihisa Yamada.