Teoria de tipus intuicionista

La teoria de tipus intuicionista, en anglès: Intuitionistic type theory (també coneguda com a constructive type theory, o Martin-Löf type theory) és una teoria de tipus i un fonament matemàtic alternatiu basada en els principis del constructivisme matemàtic. Aquesta teoria va ser presentada pel matemàtic suec Per Martin-Löf el 1972. Martin-Löf l'ha modificada unes poques vegades, la seva formulació impredicativa de l'any 1971 era inconsistent com va demostrar la Paradoxa de Girard. Formulacoons posteriors si eren predicatives.

La eoria de tipus intuicionista està basada en certes analogies o isomorfismes entre proposicions i tipus.

Aquesta teoria internalitza la interpretació de la lògica intuicionista proposada per Brouwer, Heyting i Kolmogórov, l'anomenada com BHK interpretation.

BibliografiaModifica

Enllaços externsModifica