Karl Popper’s Objective Knowledge stands at the threshold of his last major philosophical phase, the period from his retirement from the London School of Economics in 1969 until his death in 1994. The two great books that he wrote before he came to London, Logik der Forschung and The Open Society and Its Enemies, contain much more than the innovations in the theory of scientific method and the theory of democracy for which they are famous. Logik der Forschung, translated into (...) English as The Logic of Scientific Discovery, is by no means just a tract, even a revolutionary one, on the methods of science, since about one third of the text is devoted to searchingly original treatments of the frequency theory of probability and of the interpretation of quantum mechanics, whilst the unpublished manuscript on which the book was based, Die beiden Grundprobleme der Erkenntnistheorie, at whose content it often hints, presents a wealth of significant material on the psychology of human learning and its biological context. Popper had, after all, been a student of Karl B¨uhler, and had absorbed the theories of problem solving developed within the W¨urzburg School. The Open Society and Its Enemies, for its part, is not so much a book defending democratic liberalism as a defence of democratic liberalism nestling within a book that discusses every other topic under the sun. It offers profound and provocative studies of the thought of Plato and Marx, an abundance of scholarly, if often controversial, historical interpretations of the work of Heraclitus, Aristotle, Hegel, J. S. Mill, Wittgenstein, Mannheim, and others, the elements of a new theory of rationality, and many elucidations of the workings of science that go beyond what is explicit in Logik der Forschung. One insight worth mentioning, since it is little known, is the clear recognition in section II of Chapter 11 that most important advances in science are revolutionary, not cumulative; a commonplace today perhaps, but one that many philosophers attribute to Kuhn. Another insight, also often forgotten, is the emphasis in Chapter 23 on the social character of science, which acts as the main custodian of its claim to objectivity. (shrink)

Girard and Reynolds independently invented System F to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates types with untyped lambda terms, raises the questions of typability and type checking. Typability asks for a term whether there exists some type it can be given. Type checking asks, for a particular term and type, whether the term can be given that type. The decidability of these problems has been settled for restrictions and (...) extensions of F and related systems and complexity lower-bounds have been determined for typability in F, but this report is the first to resolve whether these problems are decidable for System F. This report proves that type checking in F is undecidable, by a reduction from semi-unification, and that typability in F is undecidable, by a reduction from type checking. Because there is an easy reduction from typability to type checking, the two problems are equivalent. The reduction from type checking to typability uses a novel method of constructing lambda terms that simulate arbitrarily chosen type environments. All of the results also hold for the λI-calculus. (shrink)