
About one fourth of G & ouml;del's Resultate Grundlagen is dedicated to intuitionistic and modal logic. His so far unknown results of 1941-42 on these topics contain a proof of faithfulness of the translation of intuitionistic into modal logic. The proof is purely syntactic and gives a converse to G & ouml;del's translation published in his short article of 1933, through a propositional version of Barr's theorem, a result G & ouml;del had left as a conjecture in 1933. A reconstruction of his proof is presented that extends also to derivations from assumptions and to intermediate logics. Besides providing the topological semantics of modal logic, later used by McKinsey and Tarski to prove the same embedding result by semantic means, G & ouml;del obtained many other-at the time new-results by the topological semantics, among them that there is an infinity of inequivalent propositions in one variable in intuitionistic logic.
The G & ouml;del papers contain a set of four shorthand notebooks with the title Resultate Grundlagen, with a continuous pagination from 1 to 368 and with 126 theorems. These results were obtained and written down in the years 1940-42, with about 60% belonging to set theory, and some 25% to intuitionistic logic. The nature of these notebooks and the results therein are described on the basis of transcriptions into German and translations into English of the shorthand notebooks.
Kurt G & ouml;del in 1940-42 filled four notebooks with results on foundations that he considered finished, with the German title Resultate Grundlagen. These notebooks, carefully written in the forgotten Gabelsberger shorthand, have been recently transcribed and translated into English and published under G & ouml;del's name with the title Results on Foundations. It has turned out that about 60% of these results are in set theory, with remarkable independent discoveries and anticipations of concepts and results in set theory found several decades after G & ouml;del's work.
Godel defined in 1938 and 1940 two systems of sequent calculus for implicational logic, with the aim of proving their decidability. The first calculus, from Godel's logic lectures at Notre Dame, has modus ponens among its rules, equivalent to a rule of cut, the second, from Godel's Resultate Grundlagen, an explicit rule of cut and additional groundsequents that do the work of a left implication rule. No use is made of Gentzen's method of cut elimination, and Godel's arguments are very hard to follow. Cut elimination turns out to have, indeed, methodologically interesting new aspects for Godel's second calculus, the one of the Resultate Grundlagen; It turns out that derivations with cut can be transformed into ones in which the right premiss of cut is a groundsequent, which property is shown to give the subformula property.
The topic of this paper is the role intuition can play in the mathematical practice of conjecturing. More precisely, it addresses the question of how intuitions can serve to rationally form fruitful conjectures. To succeed in making fruitful conjectures, various conditions must be fulfilled. Syntactic capacities paired with unwarranted truth claims are not sufficient. Conjecturing is not guesswork and not all intuitions are of the same relevance to it. The kind of intuition that can and often does play a leading role in the practice of conjecturing is typically invoked by experts. But even if a statement is suggested by expert intuition, the attempt to conjecture it may still fail due to insufficient justification. In such cases, one has to offer other reasons why the statement should be considered probably true and worth investigating. Although an established conjecture may of course still prove to be false, this need not undermine its fruitfulness. For in mathematics, the refutation of an interesting claim can be the proof of an equally intriguing statement. And when it comes to identifying what is potentially fruitful, intuition has again a crucial role to play. This paper aims to show that the unwritten rules, implicit criteria and intellectual powers at work in the art of conjecturing are indeed a valuable field of investigation for epistemology. It is also an attempt to contribute to the larger issue of how intuition relates to knowledge and truth in mathematics.