A Concrete Final Coalgebra Theorem for ZF Set Theory

TL;DR

This paper proves a special final coalgebra theorem within ZF set theory, replacing Aczel's Anti-Foundation Axiom with a variant that allows non-well-founded constructions, aiming for simplicity and machine implementation.

Contribution

It introduces a concrete final coalgebra theorem in ZF, replacing the Anti-Foundation Axiom with a variant definition of functions suitable for non-well-founded objects.

Findings

Proved a final coalgebra theorem in ZF set theory.

Developed a variant of functions for non-well-founded constructions.

Implemented a simple case in Isabelle theorem prover.

Abstract

A special final coalgebra theorem, in the style of Aczel's, is proved within standard Zermelo-Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's Solution and Substitution Lemmas are proved in the style of Rutten and Turi. The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. The theory is intended for machine implementation and a simple case of it is already implemented using the theorem prover Isabelle.