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

This is just to give a pre-release sneak peek of a pre-preprint I want to put on the arXiv very shortly. It’s a slightly odd beast, since I think it might be of some interest to logicians/philosophers, computer science types and possibly also category theorists, but I can’t tell. It’s a further analysis of Lawvere’s diagonal argument/fixed point theorem, reducing the assumptions beyond what is probably sensible, and giving a few different versions of the fixed point theorem more general than Lawvere’s. Here’s the abstract:

This note generalises Lawvere’s diagonal argument and fixed-point theorem for cartesian categories in several ways. Firstly, by replacing the categorical product with a general, possibly incoherent, magmoidal product with sufficient diagonal arrows. This means that the diagonal argument and fixed-point theorem can be interpreted in some substructural type theories, and semantically in categories with a product functor satisfying no coherence axioms, for instance relevance categories. The second way is by showing that both of Lawvere’s theorems as stated for cartesian categories only concern the well-pointed quotient, and giving a version of the fixed-point theorem in the internal logic of an arbitrary regular category. Lastly, one can give a uniform version of the fixed-point theorem if the magmoidal category has the appropriate endomorphism object, and has a comonad (i.e. an (S4) necessity modality) allowing for potentially `discontinuous’ dependence on the initial data.

Perhaps it is just a bit of a curio, and really waiting for a killer app, but it’s been sitting on my plate for a while, and I think some level of feedback is warranted, since I really can’t tell how it will land with people inside and outside my sphere of expertise. Grab your copy here.

2 thoughts on “Substructural fixed-point theorems and the diagonal argument: theme and variations

  1. There’s a preposition or conjunction missing in the title of section six between ‘The fixed-point theorem’ and ‘the internal logic of a regular category’

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.