Constructibility and Geometry

Abstract

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 Π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.