Document Open Access Logo

Complete Non-Orders and Fixed Points

Authors Akihisa Yamada , Jérémy Dubut

Thumbnail PDF


  • Filesize: 463 kB
  • 16 pages

Document Identifiers

Author Details

Akihisa Yamada
  • National Institute of Informatics, Tokyo, Japan
Jérémy Dubut
  • National Institute of Informatics, Tokyo, Japan
  • Japanese-French Laboratory for Informatics, Tokyo, Japan

Cite AsGet BibTex

Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
  • Order Theory
  • Lattice Theory
  • Fixed-Points
  • Isabelle/HOL


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail