| Title | Constructive and intensional logic |
|---|---|
| Period | 01 / 2001 - 01 / 2004 |
| Status | Completed |
| Research number | OND1280272 |
| - Characterization: This project continues the long-standing Amsterdam tradition in mathematical logic and the foundations of mathematics. Over the years, the original core theme of constructivism has widened to become general proof theory and provability logic, and on the other hand modal and dynamic logic. Thus, the two main 'trademarks' of mathematical logic at Amsterdam fit together in their efforts to create a general framework for reasoning and information flow. - Main themes: The first theme is concerned with foundations of constructivism, and more general proof theories emanating from that tradition. Current interests here include intuitionistic logic, type theories, linear logic and other substructural resource logics. Semantic foundations of these theories, in terms of Kripke models or categorial models, are also actively investigated. The eventual aim is a general formulation of the constructivist program as a practical general-purpose tool for the working mathematician, computer scientist, and computational linguist. Another theme is provability and interpretability logic of arithmetic, with its current ramifications into recursion theory and complexity theory, as well as 'weak arithmetics'. Topics here include interpolation properties, axiomatic completeness, and modal-style formalizations of further proof-theoretic notions. This research has close ties with the projects Algorithmics and Information Processing and Computational and Applied Logic. It also serves as a test-bed for more discriminating notions of complexity that may increase our theoretical understanding of the actual workings of automated deduction on large-scale input sets. The third theme is modal and dynamic logic. Modal logics are designed to combine reasonable expressive power with a decidable notion of validity. Special emphasis is given to dynamic logics, i.e., modal logics of action inspired by the analysis of computation and information flow. Our overall goal is a modally inspired mathematical framework for information flow, pursued in analogy with classical logic. A number of topics are studied. One is large decidable 'guarded fragments' of first-order logic, which generalize modal logics. Modal process theory on labeled transition systems is studied with a wide spectrum of process equivalences: semantic invariance and syntactic definability for process languages, expressive completeness of process repertoires with regard to bisimulation. Another topic is the use of modal techniques to reduce the complexity of logical systems by decomposing their standard semantics into a decidable logical core plus mathematical extras. The modal analysis of games as a dynamic many-agent model for communication and interaction is explored, as are modal structures in visual information. Finally, the mathematical side of modal logic, and in particular its algebraic theory, is an object of investigation. - Results 1996-1999: Within the theme of foundations of constructivism and proof theory and the connected theme of provability and interpretability logic research has concentrated on the following topics: the correspondence between normal natural deductions and normal Gentzen deductions for intuitionistic and classical logic; the Heyting algebra of Heyting arithmetic and its subalgebras, in connection with provability logic; interpolation for interpretability logics connecting this to fixed points and definability. Some new results on the provability logic of Heyting arithmetic were obtained, and a long-standing conjecture on the so-called admissible rules of intuitionistic logic was solved. Research on the theme of modal and dynamic logic produced the following results. With respect to 'guarded fragments' results on interpolation, Beth-definability, a new game semantics for fixed-point extensions, and automated theorem proving for guarded languages were obtained. A bisimulation-style first-order analysis was found for equivalence between Chu spaces that model both processes and information structure. Generalized interpolation methods were found for infinitary languages which formalize 'transfer of information' along various model relations. 'Poor man's versions' were studied for modal and first-order languages lacking disjunction and negation, which are related to modal description logics'. Within the topic of logic and game theory, a systematic analysis of game equivalences was obtained and modal-style characterizations for these, along with logical calculi for game operations, design of a common framework for logic games emphasizing players' powers and strategies, a new epistemiclogic analysis of information flow in imperfect information games, and new modal logics of coalitional power in games. Research on visual information produced a game-based version modal logic for topological spaces which measures 'distance' between pictures. This work was done in collaboration with the Institute for Informatics. - Challenges: The main challenges with the first two themes are to discover or at least approximate the provability logic of Heyting arithmetic, and to discover the interpretability logic of all reasonable arithmetic theories. Research in the third theme aims to achieve a grand view of the decidable content of first-order logic, and to collect the scattered literature on many-agent logical dynamics into one coherent logical theory of dynamics. - Plans: In interpretability and provability logic, we will look for new interpretability principles valid in all reasonable arithmetics, and investigate these principles modally, especially with regard to completeness. In the intuitionistic context interpretability has been replaced by its more positive dual form, Sigma-preservativity. This may indirectly lead to a complete solution of the problem of the provability logic of Heyting arithmetic. As for the modal fine-structure of classical logics, here we intend to push the guarded analysis of the content of first-order logic and other classical formalisms into hands-on computational experimentation. Concerning logical dynamics, processes and games, earlier dynamic logics of computation processes will be combined into one coherent theory, which will be tested on actual games. These game logics lend themselves well to computational experimentation, which opens up a new interface between logic and economic game theory and decision theory, as well as modern trends in AI. On a more abstract level, the role of modal logic in the mathematical modelling of dynamics will be investigated. This involves the study of fixed point logics, of the connection between modal logic and co-algebras, and, more at the background, the duality theory of lattices with operators. This line of research ties up with developments in the semantics of programming languages. Work on applied modal logics in specific settings, such as visual information, will continue. The motivation is not just the ubiquity of modal structures, but especially the need for a combination of various kinds of information (symbolic, visual). This requires both a logical analysis of visual structure, and a 'many-component' view of architectures for combining calculi that seem essential for a working logical theory that can cope with the two major features of realistic information: its diversity, and its bulk. |
| Researcher | Dr. H.C. Doets |
|---|---|
| Researcher | Prof.dr. A.S. Troelstra |
| Researcher | Prof.dr. Y. Venema |
| Researcher | Dr. D. Zambella |
| Project leader | Prof.dr. J.F.A.K. van Benthem |
| Project leader | Prof.dr. D.H.J. de Jongh |
| A90000 | Fundamental research |
|---|---|
| D11100 | Logic, set theory and arithmetic |
Go to page top
Go back to contents
Go back to site navigation