Skip to Main content Skip to Navigation
Conference papers

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–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.
Document type :
Conference papers
Complete list of metadata
Contributor : Jérémy Dubut Connect in order to contact the contributor
Submitted on : Thursday, November 21, 2019 - 5:17:07 PM
Last modification on : Saturday, December 4, 2021 - 3:58:02 AM



Akihisa Yamada, Jérémy Dubut. Complete Non-Orders and Fixed Points. 10th International Conference on Interactive Theorem Proving (ITP 2019), Sep 2019, Portland, United States. pp.30:1-30:16, ⟨10.4230/LIPIcs.ITP.2019.30⟩. ⟨hal-02374892⟩



Record views