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{http://isa-afp.org/entries/Complete_Non_Orders.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.