Il terzo teorema di Godel-Kreisel nella teoria intuizionistica dei tipi di Martin-Lof

The completeness of the fragment strongly denied in intuitionistic logic with respect to the intuitive semantics implies the validity of the principle of Markov in metalanguage where "intuitive semantics 'and' a free translation of naive semantics. This thesis will prove that this theorem can 'be effectively formulated and proved in the intuitionistic theory of types of P. Martin-Lof (ITT), which is exposed in detail in [MLS] and [NPS]