The approach of the Year 2000 is occasion for stock-taking all round, and that's hard to resist. But aside from that, in some subjects like proof theory, this seems to be a very appropriate time to make such an assessment.
Early in September I circulated a list of questions concerning the state and future of the subject of proof theory to about 35 workers in that field. So far, about a third of them have responded. At the Logic Lunch next Friday, I will present various of the responses received and then open up the meeting for discussion.
Here is the list of questions I sent out.
Recursive types, or self-referential types, are indispensable to understand some important features of programming languages, such as inductive (or coinductive) data structures, and self-referential objects in object-oriented programming. In particular, object-oriented languages requires even types with negative self-references. A model for such unrestricted recursive types was invented by MacQueen, Plotkin and Sethi [1983], and has been widely adopted as a basis for object-oriented typing systems.
On the other hand, it is well known that logical formulae with unrestricted self-references introduce a contradiction called Russell's paradox. Through the "formulae as types" notion, this paradox corresponds to the fact that every type is inhabited by a diverging program which does not provide any information, and implies that even with the model mentioned above, one can regard types only as partial specifications of programs, and must discuss their convergence outside of the typing system.
In this talk, a modal typing system and its realizability interpretation are proposed to capture recursive types, including such paradoxical ones, in the formulae as types notion, where the convergence of well-typed programs is ensured. Furthermore, this typing system gives such a concise description of fixed point combinators, such as Y, that one can construct recursive programs using fixed point combinators referring only to their type.
In this talk I will start by explaining briefly how dialectica categories get their name, from Goedel's dialectica interpretation. Then I present two kinds of dialectica categories in the literature and show that they are categorical models of, respectively intuitionistic and classical Linear Logic. I also describe how they compare with Chu Spaces. Finally I shall present a mild generalization of the construction and suggest some further work.
A formula is monotone if it is constructed from atomic formulas (including FALSE) by &,v and quantifiers. M. Baaz and A. Leitsch proved that the elimination of cuts over non-monotone formulas has nonelementary complexity. We simplify their proofs using pruning transformations (underlying Harrop's theorem) which allow drastically `` skolemize'' formulas proved from Horn axioms.
I will give an overview of a project whose starting point was the realization that the modern development of higher set theory necessitates an evaluation of the feasability of of Godel's program as described in his articles on Cantor's Continuum Problem and related philosophical writings. Godel suggested that a clarification of meaning of the basic notions of set theory may lead to new axioms which are "implied" by the concept of set and strong enough to decide questions that are unsolvable with the standard axioms. I will examine some candidates for axiomhood that have been proposed recently under this aspect.
The most controversial aspect of Godels philosophy of mathematics has been the epistemic weight he attaches to mathematical intuition as a form of perception of concepts. However, many of his cryptic remarks receive a natural interpretation when considered in the light of Husserl's phenomenology. In addition, I will mention another approach which is compatible with a realistic attitude towards mathematical discourse without making a commitment to the objective existence of mathematical objects or attributing perceptual character to mathematical intuition.
Finally, I will briefly describe some alternative scenarios to Godel's views of the continuum problem.