tipi, teoria dei

tipi, teoria dei

Sistema formale che Russell propose all’inizio del 20° sec. al fine di dare una soluzione al problema dei paradossi logici (➔ paradosso). Sia nella forma della teoria dei tipi ramificata (Russell) sia in quella della teoria dei tipi semplici (L. Chwistek e Ramsey), tale sistema considera la strutturazione dell’universo del discorso secondo una rigida gerarchia di tipi di oggetti (individui; insiemi; insiemi di insiemi, ecc.) dove ciò che afferisce a un determinato tipo logico può essere membro solo di qualcosa che afferisce al tipo logico immediatamente superiore. Tale locuz. è utilizzata in logica anche con riferimento a particolari calcoli (lambda calcoli) le cui espressioni (lambda termini) sono classificate in tipi. Ne sono esempi: la teoria dei t. di A. Church; la teoria intuizionista dei t. di P. Martin-Löf; il sistema F di J.Y.Girard; il calcolo delle costruzioni di T. Coquand.