Dubbio su Martin-Löf e Grothendieck.

[Pinky_Pie95]

Stavo pensando, gli universi nella teoria dei tipi di Martin-Löf (MLTT) sono in qualche modo correlati all'assioma degli universi di Grothendieck?
Per chi non ha sentito nominare nessuna delle due, gli universi in MLTT sono una gerarchia di universi Uₐ per qualsiasi n naturale per la quale Uₐ : Uₐ₊₁ con un universo U₀ che contiene tutti i tipi ``base'' tipo ℕ, ℤ, String, etc.(*) e chiusi su Π e Σ. Di solito la gerarchia è comulativa nel senso che se x : Uₐ allora anche x : Uₐ₊₁.
Un universo di Grothendieck U invece è un set transitivo (se X ∈ U e x ∈ X allora x ∈ U) per cui risulta anche vero che:
- se x ∈ U allora x ⊂ U;
- se x ∈ U e y ∈ U, {x,y} ∈ U;
- se f : X → U e X ∈ U, f[X] ∈ U (dove f[X] è l'immagine di f in X).
L'assioma degli universi di Grothendieck dice semplicemente che per ogni set x, esiste un universo di Grothendieck U per cui x ∈ U.
Questo mi fa pensare che ci sia una gerarchia simile a quella degli universi in MLTT. La domanda quindi è, limitandoci ad una qualche formulazione intuitizionistica di ZF in quanto anche MLTT lo è, i due concetti sono in qualche modo correlati oppure è solo una cosa apparente?


(*) ma non List, Vect, e altri type constructor perchè List : Π(x:U₀).U₀, Vect : Π(n:ℕ).Π(x:U₀).U₀, ed entrambi sono in U₁. Se consideriamo per esempio List(α) e Vect(n)(α) per α : U₀ e n : ℕ allora sì, sono in U₀.

[Tiger]

Ehm...
Molti qui non lavorano alla NASA... come cacchio facciamo a risponderti?

[Tiger]

Grazie al cazzo

[Sla]

Se avesse davvero voluto una risposta non avrebbe speso il 99% del post per spiegare la sua stessa domanda
troll alle prime armi.

[Jak]

Uhm, un permaban in effetti sarebbe molto utile.
Era tanto tempo che non ricevavamo forme così raffinate di trolling.

[civic71]

Secondo me come modello della teroria degli insiemi , risulta solo una cosa apparente.

Spoiler

ho vitno qualche cosa ?
http://it.wikipedia.org/wiki/Universo_di_Grothendieck

[Pinky_Pie95]

Pubblico tosto, eh? Non si possono fare due domande un po' più ostiche che subito scatta l'accusa di trolling.

Se avesse davvero voluto una risposta non avrebbe speso il 99% del post per spiegare la sua stessa domanda
troll alle prime armi.

Sono, boh, due settimane che vago negli internet in cerca di risposta (come per l'altro thread, che tra l'altro è stato proprio quello che mi ha spinto ad approfondire quest'argomento, posso tracciarti tutto il percorso mentale che ho fatto se non mi credi), avendo trovato niente, ho pensato di chiedere qui perchè non si sa mai, si potrebbe iniziare una discussione interessante o (non sia mai, per l'amor del cielo) qualcuno potrebbe essere interessato dell'argomento, ergo ho fatto un'introduzione veloce di quel che si parlava, per dare un po' di contesto. Oltretutto, ci sono varie formulazione degli universi in MLTT e alcune sono più forti delle altre, altre incompatibili tra loro, devo pur specificare quale ho in mente, no? (l'unica in cui sono abbastanza confidente, a dir la verità)

Uhm, un permaban in effetti sarebbe molto utile.
Era tanto tempo che non ricevavamo forme così raffinate di trolling.

Spoiler

Se per raffinato intendi l'unicode vario, è solo un mio fetish. In mancanza di BBCode completo e TeX, ci si deve accontentare.

Secondo me come modello della teroria degli insiemi , risulta solo una cosa apparente.

Spoiler

ho vitno qualche cosa ?
http://it.wikipedia.org/wiki/Universo_di_Grothendieck

Non capisco cosa intendi. Vuoi dire che IZF+GU != MLTT?

[Jak]

Di uno che sta sempre in chat dicendo "cocks cocks cocks" non è che mi fidi molto.
Ormai abbiamo capito la tua natura trollesca.

[Pinky_Pie95]

Non si può essere seri tutto il tempo, suvvia.
(la domanda è ancora aperta, intanto.)

[Delfador]

La risposta è: Sì.

[Tiger]

DT, la domanda, se non è uno scherzo(oramai non so più cosa pensarne ) , è piuttosto complicata da capire.
Se è uno scherzo, meriti di NON essere bannato, dato che con questi topic riesci a farmi fare la più lunghe rotolate per terra.

[Tizzio]

Ma perchè pensate sia un troll semplicemente per giustificare la vostra ignoranza...
Ha fatto una domanda, se non sapete la risposta non significa che sia una trollata.
quindi, evitate di sporcare il topic con le vostre trollate se non siete interessati all'argomento.
Non avete capito che tra qualche anno dt sarà negli iu es ei come capo-settore aerospaziale della nasa...

[Pinky_Pie95]

Entrambe le cose, la domanda è seria.

Non avete capito che tra qualche anno dt sarà negli iu es ei come capo-settore aerospaziale della nasa...

No grazie, non voglio essere un ingegnere aerospaziale sottopagato/senza lavoro.

[Tizzio]

ma non è il forum giusto.. ed è la seconda volta che glielo diciamo(dico)

non è il forum giusto anche per "Non solo fail[topic divertente]"

si vedono più fails che giochi.

[Tiger]

Su questo ha ragione.
_DT mi spiace ma non possiamo aiutarti.
Poi con l'avatar che hai, messo accanto a quelle domande assurde, è ovvio che pensano che vuoi trollare.

[CaMpIoN]

Grothendieck: http://it.wikipedia.org/wiki/Universo_di_Grothendieck
Martin-lof: chef http://www.livinginside.it/index.php?pa ... &lingua=it
xD

Guardando su wikipedia qualcosa ci ho capito, l'hai fatto un po' tu difficile, comunque, non ho trovato nulla riguardo Per Martin-Lof, tranne che quel post che parla di uno chef xD