Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Tarski's least fixed point theorem: A predicative type theoretic formulation

Ian Ray

TL;DR

This work translates Giovanni Curi's predicative least fixed point theorem into type theory and explores restrictions on monotone maps that allow for an alternative statement of the least fixed point theorem which goes beyond the version found in Curi's work.

Abstract

We provide a type theoretic treatment of the paper "On Tarski's fixed point theorem" by Giovanni Curi. There are benefits to having a type theoretic formulation apart from routine implementation in a proof assistant. By taking advantage of (higher) inductive types, we can avoid complicated set theoretic constructions. Arguably, this results in a presentation that is conceptually clearer. Additionally, due the predicative admissibility of (higher) inductive types we take a step towards the "system independent" derivation that Curi calls for in his conclusion. Finally, we explore a condition on monotone maps that guarantees they are `generated' and give an alternative statement of the least fixed point theorem in terms of this condition.

Tarski's least fixed point theorem: A predicative type theoretic formulation

TL;DR

This work translates Giovanni Curi's predicative least fixed point theorem into type theory and explores restrictions on monotone maps that allow for an alternative statement of the least fixed point theorem which goes beyond the version found in Curi's work.

Abstract

We provide a type theoretic treatment of the paper "On Tarski's fixed point theorem" by Giovanni Curi. There are benefits to having a type theoretic formulation apart from routine implementation in a proof assistant. By taking advantage of (higher) inductive types, we can avoid complicated set theoretic constructions. Arguably, this results in a presentation that is conceptually clearer. Additionally, due the predicative admissibility of (higher) inductive types we take a step towards the "system independent" derivation that Curi calls for in his conclusion. Finally, we explore a condition on monotone maps that guarantees they are `generated' and give an alternative statement of the least fixed point theorem in terms of this condition.
Paper Structure (11 sections, 16 theorems, 53 equations)

This paper contains 11 sections, 16 theorems, 53 equations.

Table of Contents

  1. Introduction
  2. Note about Predicativity
  3. Type Theoretic Framework
  4. Sup Lattices and Small Bases
  5. Inductive Generators
  6. Local Inductive Generators
  7. Least Fixed Point of Monotone Operators
  8. Bounded Inductive Generators
  9. Small-Presentation of a Lattice
  10. Predicative Least Fixed Point Theorem
  11. Conclusion

Key Result

Proposition 4.6

Consider a $\mathcal{V}$-sup-lattice L a type $A : \mathcal{V}$ and a map $m : A \to L$. Further suppose we have $S, R : \mathcal{P}_\mathcal{V}(A)$ with $S \subseteq R$ then $\bigvee S \leq \bigvee R$. Here $m \circ \text{inc}_A : \mathbb{T}(S) \to L$ is the map we are leaving implicit and similarl

Theorems & Definitions (62)

  • Definition 4.1
  • Definition 4.2
  • Definition 4.3
  • Definition 4.4
  • Example 4.5
  • Proposition 4.6
  • proof
  • Proposition 4.7
  • proof
  • Proposition 4.8
  • ...and 52 more