Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: arithmetic pretopos

Bottom of Page

1 to 14 of 14

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMay 20th 2015

    stub for arithmetic pretopos, just to record the reference

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 21st 2015
    • (edited May 21st 2015)

    We have the grey link arithmetic universe at abstract Stone duality, which we may want to redirect to arithmetic pretopos. I only don’t do it, since these are not the same thing (an AU has been defined by Joyal, though no one has seen it), even though Maietti’s proposal is that an arithmetic universe be defined as a list-arithmetic pretopos.

    I hope we can flush Joyal’s definition out of the undergrowth…

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2015

    I have added to arithmetic pretopos the redirect and the sentence

    Maietti proposed that arithmetic pretoposes serve as the arithmetic universes that Andre Joyal once suggested to use for discussion of incompleteness theorems.

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 21st 2015

    Alright :-). I guess there’s not much to discuss…

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 21st 2015
    • (edited May 21st 2015)

    Trying to unwind Maietti’s definition of parameterised list objects, I guess they are just W-types for the non-locally cartesian closed version of the polynomial functor giving list objects. Cockett (JPAA 1990) defines them as initial algebras for the endofunctor B+A×(−)B+A\times (-) (for arbitrary AA and BB).

    Let me edit that in now… (EDIT: done!)

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2015
    • (edited May 21st 2015)

    Thanks!

    Gave hyperlinks to you finite products and (more importantly) disjoint coproducts.

    • CommentRowNumber7.
    • CommentAuthorThomas Holder
    • CommentTimeApr 23rd 2020

    Added a reference to

    • {#vanDijkOldenziel20} Joost vaan Dijk, Alexander Gietelink Oldenziel, Gödel incompleteness through Arithmetic Universes after A. Joyal , arXiv:2004.10482 (2020). ((abstract)

    diff, v11, current

  8. Thanks very much Thomas! Fantastic that somebody has written up the details of this, I and many people have long wished to see the argument. I’d like to work through it when I get the chance and put some details on the nLab.

  9. See here for an old nForum discussion around this.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 23rd 2020

    Re #7: I’ve just posted something on this at MO.

  11. The link to Maria Maietti’s draft of “Modular correspondence between dependent type theories and categories including pretopoi and topoi” doesn’t work anymore, it leads to a “Page not found”

    Anonymouse

    diff, v14, current

  12. Unfortunately, the Wayback Machine doesn’t seem to have the article stored in its archive:

    https://web.archive.org/web/20230000000000*/https://www.mittag-leffler.se/preprints/files/IML-0001-44.pdf

    Anonymouse

    diff, v14, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 13th 2023

    On my system, the first hit when googling for the title is the working pdf here.

    I have added also the doi:10.1017/S0960129505004962.

    diff, v15, current

    • CommentRowNumber14.
    • CommentAuthorJohn Baez
    • CommentTimeMay 28th 2024

    Added proposal by Sridhar Ramesh for formulating first-order PA using a pretopos with parametrized natural numbers object.

    diff, v16, current

1 to 14 of 14

  1.