Michele Contente: Some remarks on the constructive conception of predicativity

Organized by the Department of Logic

Further information

Michele Contente (FLÚ AV ČR):
Some remarks on the constructive conception of predicativity

The notion of predicativity emerged in the early 20th-century debate on paradoxes. From a foundational perspective, a key development has been the proof-theoretical analysis of the notion of predicativity ("given the natural numbers") conducted by Feferman and Schütte, which led to the identification of a limit ordinal for predicative theories. Nowadays, predicative theories are primarily employed in the foundations of constructive mathematics. Examples include CZF and various versions of Martin-Löf's type theory. In these theories, constructions that are not predicatively admissible according to the classical proof-theoretical conception are considered fully legitimate, thus giving rise to a constructive notion of generalized predicativity. The talk aims to analyze the resulting notion of predicativity mainly in the context of Martin-Löf's type theory.