Arithmetic universes: Home of free algebras

Add to your list(s) Download to your calendar using vCal

• Steve Vickers, CS Theory Group Birmingham
• Friday 20 November 2020, 14:10-15:10
• Zoom. To join mailing list for updates (including Zoom links), please send your details to palmgren-memorial@math.su.se in advance.

If you have a question about this talk, please contact Dr Steve Vickers.

Given as invited contribution to the Erik Palmgren memorial conference, 19-21 Nov 2020

(This talk is given as an invited contribution to the Erik Palmgren memorial conference, 19-21 Nov 2020.)

Every algebraic theory (operators and equational axioms) has an initial model using a well known term/congruence construction, a term algebra modulo a congruence generated from the axioms. The result also holds (see Barr and Wells) for finite limit theories, aka cartesian or essentially algebraic; however, the term/congruence proof breaks down. Operators may be partial, and factoring out the congruence may cause new terms to be defined.

In my 2007 paper with Erik Palmgren, “Partial Horn logic and cartesian categories”, we showed how to simplify the development using a logic of partial terms, with definedness as self-equality. In this logic the term/congruence process uses partial terms and a partial congruence, and does construct an initial model. One class of cartesian theories that we discussed is that of category with structure and internal T-model, and the initial model is then a classifying category for T.

In my talk I shall focus on Joyal’s arithmetic universes (AUs), pretoposes with parametrized list objects. They face two ways. On the one hand, the theory of AUs is cartesian. On the other, the internal logic of AUs is sufficient to support our term/congruence construction of initial models. I shall present an overview of facts, conjectures, and mysterious phenomena. These include internalization (Joyal’s original motivation, for Goedel’s Incompleteness Theorem) and applications to base-independent geometric logic and classifying toposes.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• Zoom. To join mailing list for updates (including Zoom links), please send your details to palmgren-memorial@math.su.se in advance
• computer sience

Note that ex-directory lists are not shown.