Induction, Coinduction, and Fixed Points: A Concise Comparative Survey

TL;DR

This survey compares induction and coinduction principles across multiple mathematical disciplines to clarify their similarities and differences, and explores potential unification via category theory concepts.

Contribution

It provides a comprehensive comparison of induction and coinduction in various frameworks and discusses prospects for a unified categorical approach.

Findings

Identifies key similarities and differences between disciplines

Highlights the role of fixed points, algebras, and coalgebras

Suggests potential for a unified categorical treatment

Abstract

In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, set theory, programming languages' type theory, first-order logic, and category theory, for the purpose of examining some of the similarities and, more significantly, the dissimilarities between these various mathematical disciplines, and hence shed some light on the precise relation between these disciplines. Towards that end, in this article we discuss plenty of related concepts, such as fixed points, pre-fixed points, post-fixed points, inductive sets and types, coinductive sets and types, algebras and coalgebras. We conclude the survey by hinting at the possibility of a more abstract and unified treatment that uses concepts from category theory such as monads and comonads.