typeteori

Typeteori er en logisk teori udviklet i 1900-tallets begyndelse af Bertrand Russell som et svar på det såkaldte Russells paradoks.

Det centrale i dette paradoks består i, at man for at bestemme omfanget af mængden R må undersøge, om R selv tilhører R. Løsningen består i at forlange, at elementerne i en mængde har en lavere type end mængden selv. Hvis konkrete objekter har type 0, så har mængder af objekter type 1, mængder af mængder type 2 osv. I typeteorien er det således udelukket, at R kan være element i sig selv, idet Rs elementer skal have en lavere type end R selv.

Senere i 1900-tallet benyttede Kurt Gödel typeteori til at udvikle en fortolkning af konstruktiv matematik. Typeteori er et nyttigt værktøj i matematisk grundforskning og i datalogi.