Constructivity and Predicativity: Philosophical Foundations

The thesis examines two dimensions of constructivity that manifest themselves
within foundational systems for Bishop constructive mathematics: intuitionistic
logic and predicativity. The latter, in particular, is the main focus of the thesis.
The use of intuitionistic logic affects the notion of proof : constructive proofs may
be seen as very general algorithms. Predicativity relates instead to the notion of set:
predicative sets are viewed as if they were constructed from within and step by step.
The first part of the thesis clarifes the algorithmic nature of intuitionistic proofs,
and explores the consequences of developing mathematics according to a constructive
notion of proof. It also emphasizes intra-mathematical and pragmatic reasons
for doing mathematics constructively. The second part of the thesis discusses predicativity.
Predicativity expresses a kind of constructivity that has been appealed to
both in the classical and in the constructive tradition. The thesis therefore addresses
both classical and constructive variants of predicativity. It examines the origins of
predicativity, its motives and some of the fundamental logical advances that were
induced by the philosophical re
ection on predicativity. It also investigates the relation
between a number of distinct proposals for predicativity that appeared in
the literature: strict predicativity, predicativity given the natural numbers and constructive
predicativity. It advances a predicative concept of set as unifying theme
that runs across both the classical and the constructive tradition, and identifies it
as a forefather of a computational notion of set that is to be found in constructive
type theories. Finally, it turns to the question of which portions of scientifically
applicable mathematics can be carried out predicatively, invoking recent technical
work in mathematical logic.