representation of proofs, in particular those of substructural logics, in structures of category theory, especially structures close to geometry, application of the results obtained in normalization and in deciding equality of proofs, which is important for the semantics of programming languages, investigations in the field of countable structures (Vaught's Hypothesis), elimination of quantifiers of concrete structures, theory of compact spaces that can be realized in the first Baire category of real functions, theory of approximate homomorphisms
Categorial proof theory is a field of mathematical logic that uses category theory, a very general algebraic theory, in order to describe logical systems that arise in proof theory. It is particularly interesting to find concrete categories that serve as models of abstract, "syntactic", categories inspired by logic. Such categories, which are often of a geometric type, yield a considerable simplification of the normalization procedure for proofs, and of the decision procedure for equality of proofs. These procedures, which have up to now been developed in proof theory and in the lambda calculus in a syntactical manner, are very important for computer science, because starting from them one can build methods for the verification of correctness of programs. Contemporary programming languages are based on logical languages, and logical results can be transferred to them. Verification of programs is a major goal in the semantics of programming languages, for the simple reason that the correctness of many programs cannot be empirically tested (for example, programs that may endanger human lives). Substructural logics make a family of nonclassical logics among which linear logic, inspired by computer science, is best known. These logics have especially interesting categorial models, and in this investigation we would concentrate on these models. (What we have here are models of proofs, and not models of theorems.) Geometrical categorial models connected to skein spaces and Temperley-Lieb algebras are of particular interest. These models may lead to applications in quantum mechanics. Investigations in the project would be in this area, and would concentrate in particular on the following topics: coherence in bicartesian categories, coherence in substructural categories, generalization of natural transformations, axiomatizations of categories of tangles of finite and infinite skein spaces, their connection with the notion of self-adjunction, Post completeness of monoids and other structures that arise in that context, and matrix representations of Temperley-Lieb algebras and braid groups. Besides that, the lambda calculus with intersection types would be investigated. In classical model theory, work would be pursued on Vaught's Hypothesis, and in infinite combinatorics the compact spaces mentioned above would be investigated.
The attempt to build within categorial proof theory a geometric categorial proof theory is original. This is not only of theoretical, but also of practical interest for computer science.
The goal of the research is first of all a complete geometrization of proofs, with original applications in computer science. If reached, this goal could prove tremendously important. It would enable the semantics of programming languages to leave the area of syntactic methods, to which it was tied up to now. This is comparable to what analytic geometry achieved in the seventeenth century, but in the opposite direction.
Categorial proof theory is pursued nowadays by a group of algebraists and logicians in Northern America, especially in Montreal, in Quebec, and by a certain number of mathematicians in Scotland, Australia, France, Russia, Italy and Holland. Stress on the connection between category theory and proof theory is, however, especially marked in Montreal and Belgrade. A great number of logicians and computer scientists work in the area of substructural logics, in particular in the USA, in Australia and in France. Until recently, these investigations were not classified as belonging to the same field. A unified approach was reached in the 1990s (in the Mathematics Subject Classification of the American Mathematical Society for the year 2000 appeared for the forst time two entries, 03B47 and 03F52, for substructural logics; the term "substructural logics" was introduced in 1990 by the proposer of this project). Classification of structures, the second theme of this project, is today the leading theme of classical model theory, the dominant discipline of mathematical logic in the second half of the twentieth century. It is closely tied to algebra. Investigations in this field are very much influenced by Shelah, from Israel, whose work inspires many logicains in the USA, France, Russia, Canada, etc. Infinite combinatorics is one of the most lively fields of set theory, the discipline that has characterized most of all the mathematics of the twentieth century.
Investigations in these areas in Serbia are on a very high level. Here there is no import of foreign know-how, but Serbian scientists often lead the field. Many of them have left the country not because they asked for it, but because foreigners needed their expertise and invited them (paying them well). In the fields covered by this project it is required that existing research, which has already a solid reputation in the world, be kept alive. It is required that the Belgrade schools of categorial proof theory, model theory and set theory continue to exist and exert influence in the world. Their closing would be a great loss for the country, and the achieved economy nil.
The description of the planned results is given before. The precise users of these results can, however, hardly be named at this point. They are both in theoretical fields and in fields of applied mathematics. A very long experience in mathematics - and there is no reason to believe that things will change in that respect - teches us that between results and their applications there is a period much longer than three years, which is the imposed duration of this project.