Fixed Points Theorems for Non-Transitive Relations

TL;DR

This paper develops a highly general Isabelle/HOL library for order-theoretic fixed-point theorems, extending classical results to broader classes of relations and demonstrating the completeness of fixed points sets.

Contribution

It generalizes and strengthens classical fixed-point theorems by formalizing them for non-transitive relations in Isabelle/HOL.

Findings

Generalized fixed-point theorems for complete relations.

Proved the set of fixed points is itself complete.

Unified various classical theorems under a broader framework.

Abstract

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.