It is by now well known that Gödel first advocated the philosophy of Leibniz and then, since 1959, that of Husserl. This raises three questions:

1. 1. How is this turn to Husserl to be interpreted? Is it a dismissal of the Leibnizian philosophy, or a different way to achieve similar goals?

2. 2. Why did Gödel turn specifically to the later Husserl's transcendental idealism?

3. 3. Is there any detectable influence from Husserl on Gödel's writings?

Regarding the first question, Wang [96, p.165] reports that Gödel ‘[saw] in Husserl's work a method of refining and consolidating Leibniz' monadology’. But what does this mean? In what for Gödel relevant sense is Husserl's work a refinement and consolidation of Leibniz' monadology?

The second question is particularly pressing, given that Gödel was, by his own admission, a realist in mathematics since 1925. Wouldn't the uncompromising realism of the early Husserl's Logical investigations have been a more obvious choice for a Platonist like Gödel?

The third question can only be approached when an answer to the second has been given, and we want to suggest that the answer to the first question follows from the answer to the second. We begin, therefore, with a closer look at the actual turn towards phenomenology.

Some 30 years before his serious study of Husserl began, Gödel was well aware of the existence of phenomenology. Apart from its likely appearance in the philosophy courses that Gödel took, it reached him from various directions.

Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal formin natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic.

The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well.

The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic.