Re: Algebraic closures and arithmetic universes

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

Dear Andre,

Here's my own understanding of the history of AU definitions. Can you comment on its accuracy?

1. You defined the initial AU, with a concrete construction, as sufficient structure to embody arithmetic. You also showed that the initial AU has an internal initial AU, and used that to establish the Goedel gap between truth (external) and provability (internal).

2. You and others also discussed what the general definition might be. I picked this up from Gavin Wraith in the 1990s. (I had first learned about AUs from Gavin's talk at the 1985 Surrey conference on Categories in Computer Science.) Conceptually, it was "pretopos + free algebra constructions", but the  question was how to get a collection of primitive constructions sufficient to get whatever else was needed. Gavin suggested free categories over directed graphs and free category actions over graph actions.

3. Milly Maietti proposed parametrized list objects, and I am persuaded her axiomatization is good. It is the one we used in our joint paper, and I used in "Sketches for AUs". I believe it provides adequate foundations for my proof with Palmgren of the existence of initial algebras for cartesian theories.

All the best,

Steve.

> On 1 Aug 2017, at 01:26, a1078662@adelaide.edu.au wrote:
> 
> Hi,
> 
> There's a question at MathOverflow on the construction of algebraic
> closures in constructive mathematics by Joyal. The idea as far as I can
> tell is to construct the classifying arithmetic universe for the theory of
> the algebraic closure. People might either be interested or have something
> to contribute
> 
> https://mathoverflow.net/q/277551/4177
> 
> I repeat my respectful call for André to release his notes of arithmetic
> universes for us all to use, or at the least confirm that Maietti et al
> found the same definition  :-)
> 
> 
> Best regards,
> David
> 



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]