@inproceedings{87051cd8b49e4dfd873e1d8b7a8c2680,
title = "Complete non-orders and fixed points",
abstract = "In this paper, 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 property of ordering, thus complete non-orders. In particular, we generalize the Knaster{\textendash}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 {\textendash} attractivity {\textendash} which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene{\textquoteright}s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene{\textquoteright}s fixed points are least quasi-fixed points.",
keywords = "Fixed-points, Isabelle/HOL, Lattice theory, Order theory",
author = "Akihisa Yamada and J{\'e}r{\'e}my Dubut",
note = "Publisher Copyright: {\textcopyright} Akihisa Yamada and J{\'e}r{\'e}my Dubut.; 10th International Conference on Interactive Theorem Proving, ITP 2019 ; Conference date: 09-09-2019 Through 12-09-2019",
year = "2019",
month = sep,
day = "1",
doi = "10.4230/LIPIcs.ITP.2019.30",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "John Harrison and John O'Leary and Andrew Tolmach",
booktitle = "10th International Conference on Interactive Theorem Proving, ITP 2019",
}