Complete Non-Orders and Fixed Points

 

Title: Complete Non-Orders and Fixed Points
Authors: Akihisa Yamada (akihisa /dot/ yamada /at/ aist /dot/ go /dot/ jp) 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