En logique mathématique, le System U et le System U - sont des systèmes de types purs, c'est-à-dire des formes spéciales d'un avec un nombre arbitraire de sortes, d'axiomes et de règles (ou de relations entre les sortes). Ils ont tous deux été prouvés incohérents par Jean-Yves Girard en 1972. Ce résultat conduit alors à ce que la théorie des types de Martin-Löf de 1971 est incohérente car elle permet le même comportement de «type dans le type» que le paradoxe de Girard exploite. (fr)
En logique mathématique, le System U et le System U - sont des systèmes de types purs, c'est-à-dire des formes spéciales d'un avec un nombre arbitraire de sortes, d'axiomes et de règles (ou de relations entre les sortes). Ils ont tous deux été prouvés incohérents par Jean-Yves Girard en 1972. Ce résultat conduit alors à ce que la théorie des types de Martin-Löf de 1971 est incohérente car elle permet le même comportement de «type dans le type» que le paradoxe de Girard exploite. (fr)