Jérémy Dubut ; Akihisa Yamada - Fixed Points Theorems for Non-Transitive Relations

lmcs:6809 - Logical Methods in Computer Science, February 4, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:30)2022
Fixed Points Theorems for Non-Transitive RelationsArticle

Authors: Jérémy Dubut ; Akihisa Yamada

    In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.


    Volume: Volume 18, Issue 1
    Published on: February 4, 2022
    Accepted on: January 27, 2022
    Submitted on: September 29, 2020
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1841 times.
    This article's PDF has been downloaded 787 times.