Phenomenology and transcendental argument in mathematics: the case of Brouwer's Bar Theorem
Résumé
On the intended interpretation of intuitionistic logic, Heyting's Proof Interpretation, a proof of a proposition of the form p -> q consists in a construction method that transforms any possible proof of p into a proof of q. This involves the notion of the totality of all proofs in an essential way, and this interpretation has therefore been objected to on grounds of impredicativity (e.g. Gödel 1933). In fact this hardly ever leads to problems as in proofs of implications usually nothing more is assumed about a proof of the antecedent than that it indeed is one, and this assumption does not require a further grasp of the totality of proofs. The prime example of an intuitionistic theorem that goes beyond that assumption is Brouwer's proof of the 'bar theorem': For every tree x, if x contains a decidable subset of nodes such that every path through the tree meets it (a 'bar'), then there is a well-ordered subtree of x that contains a bar for the whole of x. Instantiated with an arbitrary tree t, this proposition takes the form P(t) -> Q(t). Brouwer's proof of the bar theorem mainly consists in an analysis of the inner structure that a proof of P(t) must have, where proofs are taken to be primarily mental objects. So here Brouwer engages in phenomenological reflection by considering the acts in which we think about bars. From that analysis he obtains the information from which to construct a proof of Q(t). In this talk I will argue that Brouwer circumvents the problem of impredicativity by resorting to a transcendental argument based on phenomenological description, and defend this application by showing how common objections to transcendental arguments do not apply here. Finally, I will indulge in some historical speculation by relating the foregoing considerations to the remarkable change that Gödel's view on the Proof Interpretation underwent between his Yale Lecture (1941) and the Dialectica paper (1958).
Loading...