Co to jest super wszechświat?

9

Czytam ten dobrze znany artykuł o wszechświatach w teorii typów . Na początku spodziewałem się czegoś podobnego do SetωAgdy, ale okazuje się, że jest to nawet coś bardziej ogólnego. Wydaje się uogólniać konstrukcję wszechświata od zwykłego typu indukcyjno-rekurencyjnego do spoiwa (podobnego doΠ i Σ). Główne pytanie, które chcę zadać, to jaki jest tego zamiar?

Oto kod Idris definiujący zwykłe wszechświaty w stylu Tarskiego:

mutual

  public export data U : (level : Nat) -> Type where
    GroundU : Ground -> U level
    BinderU : Binder -> (a : U level) -> (b : (x : T {level} a) -> U level) -> U level
    UnivU   : U (S level)
    LiftU   : U level -> U (S level)

  public export T : {level : Nat} -> (code : U level) -> Type

Próbuję uogólnić na coś takiego

mutual

  public export data U : (a : Type) -> (b : (x : a) -> Type) -> Type where
    GroundU : Ground -> U a ???
    ...

Co powinno ???być Autor artykułu powiedział właśnie, że wszechświaty powinny być zamknięte pod ustalonymi twórcami.

edycja: Myślę, że ???jest po prostu b...

盛安安
źródło
Czy próbujesz mieć więcej niż Natwiele wszechświatów? Nie jest jasne, o co pytasz.
Andrej Bauer,
Papier wydaje się to robić.
盛安安
1
Wiem co jest w gazecie. Co ty próbujesz zrobić? Jakie jest Twoje pytanie?
Andrej Bauer
Cóż ... wpadłem na pomysł, który mógłby wykorzystać Setω, więc poszukałem artykułów na temat superwszechświatów, aby sprawdzić, czy mogę się czegoś nauczyć. Jest naprawdę niewiele artykułów na ten temat, a ten jest najważniejszy. Aby to zrozumieć, sam próbowałem to wdrożyć. Chociaż teraz nie sądzę, by zapewniło to wgląd w mój nowy pomysł, nadal chcę to zrozumieć.
盛安安
Chcę poznać zamiar uogólnienia budowy wszechświata na spoiwo.
盛安安

Odpowiedzi:

11

Jednym z celów stojących za zamkniętym pod nim operatorem wszechświata i superwszechświatem jest podanie teoretycznej wersji dużych kardynalnych aksjomatów znanych z teorii mnogości. Liczba nieosiągalna jest jak typ-teoretyczny wszechświata. Kolejnym interesującym rodzajem kardynała jest kardynał Mahlo . Mówiąc intuicyjnie, kardynał Mahlo to taki, który ma pod sobą „całą masę” niedostępnych kardynałów. Co by to było w kategoriach teoretycznych? To powinien być jakiś wszechświatUz dużą ilością wszechświatów. Do tego zmierza Palmgren, gdy rozważa superwszechświaty.

Istnieje również bardziej praktyczna strona posiadania wielu wszechświatów. Przydatne jest posiadanie typów indukcyjno-rekurencyjnych w teorii typów do różnych celów. Ale pozwalają nam zdefiniować nowe wszechświaty, więc pytanie brzmi: ile ? Aby poczuć, co robi Palmgren, zamiast od razu strzelać do superwszechświata, wypróbuj następującą sekwencję konstrukcji w Agda (używając rekurencji-indukcji):

  1. Zdefiniuj jeden wszechświat U0, zawierający (kod) N i zamknięty pod Π i Σ. Ten rodzaj wszechświata odpowiada niedostępnemu kardynałowi .

  2. Zdefiniuj operatora U który przyjmuje dowolny typ A i definiuje wszechświat, który zawiera (kod) A i jest zamknięty pod Π i Σ. Ten rodzaj operatora wszechświata jest podobny do aksjomatu wszechświatów Grothendiecka . Ile wszechświatów możemy uzyskać poprzez wielokrotne stosowanieU, zaczynając od N?

  3. Aby uzyskać jeszcze więcej wszechświatów, postulujemy superwszechświat V który zawiera wiele wszechświatów, jak następuje:

    • V zawiera Ni jest zamknięty pod Π i Σ
    • Podany (kod) typ A:V i rodzina B:AVistnieje wszechświat U, który jest elementem V, zawiera wszystkie typy rodziny Bi jest zamknięty pod Π i Σ.

    Ile wszechświatów robi Vzawierać? Pamiętaj, że możemy dostać rodzinęB:NV takie, że B(n) jest n-ty wszechświat i tak dalej V musi zawierać wszechświat Uωktóry zawiera je wszystkie. A to dopiero początek!

Andrej Bauer
źródło
Czy identyfikujesz Nwe wszechświecie z tradycyjnym poziomem indeksu metaoretycznego?
盛安安
Wydaje
W całym tekście korzystałem z notacji matematycznej. W ASCII pisałbym natzamiastN, więc nie jest metateoretyczny, to tylko rodzaj liczb naturalnych. To nawet nie ma tak dużego znaczenia, że ​​masz nat, użyłem go jako podstawowego typu, od którego możemy zacząć. Gdybym użył bool, również byś się czuł (z wyjątkiem gdybyś musiał przejść jeden wszechświat wyżej, aby dostać się do nieskończonych typów, ponieważ pierwszy wszechświat zawierałby tylko typy skończone zbudowane z boolużyciaΠ i Σ).
Andrej Bauer,