Constructibility and geometry
pp. 123-161
in: Gabriele Lolli, Marco Panza, Giorgio Venturi (eds), From logic to practice, Berlin, Springer, 2015Abstract
A comparison is made between logical notions of constructivity and the traditional Euclidean conception of geometry as a science of constructions. In particular, it is investigated whether the actions performable by an abstract human geometer can already be captured, at a more syntactic level, by some logical notions of constructivity. Three of these notions are analyzed: (i) intuitionistic admissibility; (ii) provability by finitistic, direct, or effective means; and (iii) algorithmic executability. Two results are then presented. On the one hand, it is shown how a plausible characterization of geometrical constructivity can be achieved by combining all three previous features. On the other hand, through a comparison with arithmetic, it is argued that geometry is essentially characterized by hypothetical and potential constructions: geometrical objects are not effectively constructed, but they are only constructible. This latter result is mainly achieved via the analysis of the existential witness extraction for (Pi _{2}) sentences. This property, which is usually considered as emblematic of proof-theoretical and syntactic approaches to constructivity, represents in fact the vestige of a referentialist position which seems to be dispensable for the description of geometrical practice.