Complete Non-Orders and Fixed Points

 Title: Complete Non-Orders and Fixed Points Authors: Akihisa Yamada and Jérémy Dubut Submission date: 2019-06-27 Abstract: We develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any properties of ordering, thus complete non-orders. In particular, we generalize the Knaster–Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition—attractivity—which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points. BibTeX: @article{Complete_Non_Orders-AFP, author = {Akihisa Yamada and Jérémy Dubut}, title = {Complete Non-Orders and Fixed Points}, journal = {Archive of Formal Proofs}, month = jun, year = 2019, note = {\url{https://isa-afp.org/entries/Complete_Non_Orders.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License