

Proof-theoretic semantics and feasibility
pp. 135-157
in: Jacques Dubucs, Michel Bourdeau (eds), Constructivity and computability in historical and philosophical perspective, Berlin, Springer, 2014Abstract
It is well known that classical mathematics have been widely criticised by the proponents of constructive mathematics on the ground that the former rests on a realist conception of the realm of mathematical objects. It must be recalled that the latter is not completely immune to such a reproach inasmuch as some vestige of realism is still present in its foundations (1). This realism takes the form of two different idealisations of human abilities: the creative ones and the mechanical ones (1.1). It can be argued that the first idealisation is avoided by the proof theoretic-semantics of constructive mathematics but not the second one (1.2). Different definitions of feasible functions and systems of feasible mathematics have been proposed that makes possible to avoid the second idealisation too (2). It is of special interest to see if they allow, at least partially, some proof-theoretical semantics (2.2).