Constructive recursive functions, Church's thesis, and Brouwer's theory of the creating subject

afterthoughts on a Parisian joint session

Göran Sundholm

pp. 1-35

in: Jacques Dubucs, Michel Bourdeau (eds), Constructivity and computability in historical and philosophical perspective, Berlin, Springer, 2014

Abstract

The first half of the paper discusses recursive versus constructive functions and, following Heyting, stresses that from a constructive point the former cannot replace the latter. The second half of the paper treats of the Kreisel-Myhill theory CS for Brouwer's Creating Subject, and its relation to BHK meaning-explanations and Kripke's Schema. Kripke's Schema is reformulated as a principle and shown to be classically valid. Assuming existence of a verification-object for this principle, a modification of a proof of conservativeness of Van Dalen's, is shown to give a relative BHK meaning explanation for the Kreisel-Myhill connective. The result offers an explanation of why Kripke's Schema can be used as a replacement of the Theory of Creating Subject when formulating Brouwerian counter-examples. It also shows that the Theory of Creating Subject is classically valid.

Cited authors

Brouwer Luitzen Egbertus Jan