Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Substructural fixed-point theorems and the diagonal argument: theme and variations

David Michael Roberts

TL;DR

The paper investigates how Lawvere's fixed-point theorem and Cantor-style diagonal arguments can be realized under weaker, substructural assumptions by using magmoidal categories with diagonals instead of cartesian products. It develops a minimal, semantically grounded framework, presents numerous noncartesian examples, and derives diagonal and fixed-point results in this setting, including internal-logical formulations in regular categories and uniform constructions via a copointed modality. Key contributions include a magmoidal formulation of the diagonal argument, a reduction to concrete cartesian quotients, and a route to uniform fixed-point constructions, connecting substructural logic with categorical fixed-point phenomena. These results broaden the applicability of diagonal-type reasoning, offer new perspectives on the role of structure in fixed points, and suggest links to lambda-calculus semantics and modality-inspired interpretations.

Abstract

This article re-examines Lawvere's abstract, category-theoretic proof of the fixed-point theorem whose contrapositive is a `universal' diagonal argument. The main result is that the necessary axioms for both the fixed-point theorem and the diagonal argument can be stripped back further, to a semantic analogue of a weak substructural logic lacking weakening or exchange.

Substructural fixed-point theorems and the diagonal argument: theme and variations

TL;DR

The paper investigates how Lawvere's fixed-point theorem and Cantor-style diagonal arguments can be realized under weaker, substructural assumptions by using magmoidal categories with diagonals instead of cartesian products. It develops a minimal, semantically grounded framework, presents numerous noncartesian examples, and derives diagonal and fixed-point results in this setting, including internal-logical formulations in regular categories and uniform constructions via a copointed modality. Key contributions include a magmoidal formulation of the diagonal argument, a reduction to concrete cartesian quotients, and a route to uniform fixed-point constructions, connecting substructural logic with categorical fixed-point phenomena. These results broaden the applicability of diagonal-type reasoning, offer new perspectives on the role of structure in fixed points, and suggest links to lambda-calculus semantics and modality-inspired interpretations.

Abstract

This article re-examines Lawvere's abstract, category-theoretic proof of the fixed-point theorem whose contrapositive is a `universal' diagonal argument. The main result is that the necessary axioms for both the fixed-point theorem and the diagonal argument can be stripped back further, to a semantic analogue of a weak substructural logic lacking weakening or exchange.

Paper Structure

This paper contains 11 sections, 8 theorems, 15 equations.

Table of Contents

  1. Outline
  2. More technical introduction
  3. Acknowledgements
  4. Products in a general setting
  5. Examples of magmoidal categories
  6. The diagonal argument in the magmoidal setting
  7. The fixed-point theorem in the magmoidal setting
  8. Reduction to a concrete category in the cartesian setting
  9. The fixed-point theorem in the internal logic of a regular category
  10. Getting a uniform construction of the fixed point
  11. Coda

Key Result

Theorem 11

For $(C,\#,\delta,t)$ a pointed magmoidal category with diagonals, and $\sigma \colon C\to C$ a $t$-free endomorphism, every $F\colon A\# A \to C$ is an incomplete parametrisation of maps $A\to C$.

Theorems & Definitions (34)

  • Example 1
  • Remark 2
  • Definition 3
  • Definition 4
  • Example 5
  • Example 6
  • Example 7
  • Example 8
  • Example 9
  • Definition 10
  • ...and 24 more