Major Scientific Accomplishments

Major scientific accomplishments

2000. Reflexive lambda-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into typed lambda-terms is a simple instance of an internalization property of a our system  lambda-infinity which unifies intuitionistic propositions (types) with  lambda-calculus and which is capable of internalizing its own derivations as lambda-terms. We establish confluence and strong normalization of lambda-infinity. The system lambda-infinity is confluent and strongly normalizable (a joint result with J.Alt) , considerably extends the expressive power of each of its major components: typed lambda-calculus, intuitionistic and modal logic. It may be regarded as the pure lambda version of the Logic of Proofs LP (cf. below). Reflexive lambda-calculus is likely to change our conception of the appropriate syntax and semantics for ambda-calculus based programming languages, systems of automated deduction and formal verification.

1999. An explicit provability model for verification.

The traditional (implicit) provability model leaves a certain loophole in the foundations of formal verification. Namely, by the Goedel Incompleteness Theorem an extension of a verification system by a verified rule generally speaking is not equivalent to the original system. This model leads to a “reflection tower” of metatheories of increasing proof-theoretical strength which itself cannot be verified formally. One has to believe in correctness of a verification system the way we believe in consistency of a set theory.

The CADE paper (cf. the list of publications) introduced the explicit reflection rule sufficient for verification purposes. The explicit reflection is internally provable, which circumvents the Incompleteness Theorem. This provides a theoretical justification of formal verification and shows how to adjust the existing methods to avoid the “reflection tower”. The possibility of implementation of this explicit reflection mechanism is now being studied for the next generation of automated problem-solving systems (Nurpl 5 and MetaPrl) by PRL-team under R. Constable at the Computer Science Department of Cornell University.

1995-1999. The discovery of a fundamental connection between modal logic and typed lambda-calculi according to which the major modal logics (K, K4, S4, S5) are nothing but implicit specifications of a families of lambda-terms standing for operations on proofs. It has been established that together with simple procedures recovering explicit proof terms from modal derivations modal logic subsumes intuitionistic and combinatory logic, typed lambda-calculus and modal lambda-calculus.

1997. A modal logic for topological dynamic systems (joint papers with Nerode and Davoren). This logic provides a framework for synthesis and verification of hybrid control systems. The dynamic variant of this logical system developed further by Davoren has been applied at the Center for Foundations of Intelligent Systems at Cornell University and in the Electronics Research Laboratory at UC Berkeley.

1994-1998. A solution to Goedel’s provability problem.

Provability has the format of a logical connective: if F is a sentence then F is provable is again a sentence. In addition to its foundational significance, provability plays an important role in such areas as knowledge representation, formal verification, nonmonotonic reasoning, constructive semantics, etc. Finding a complete system of axioms for provability has been one of the fundamental open problems. In 1933 Goedel introduced a modal calculus (also known as S4) axiomatizing provability and noticed    that the straightforward understanding of his calculus contradicted the Second Incompleteness theorem. Since then the problem of finding a rigid provability semantics for Goedel’s calculus attracted many researchers: Goedel (1933, 1938), Lemmon (1957), Kripke (1963), Montague (1963), Mints (1974), Kuznetsov (1977), Goldblatt (1978), Boolos (1979, 1993) and others. Note that the logic of formal provability introduced by Solovay and Boolos in the 1970s addresses a different issue and it is not compatible with Goedel’s provability calculus.

The solution to the Goedel provability problem has been given by an explicitly defined system of proof polynomials representing all  invariant operations on proofs. Such a solution was anticipated by Goedel in 1938 (first published in 1995). These results commended for their excellence by the Committee for the IGPL/FoLLI Prize “The Best Idea of the Year” in 1996 and were awarded the Spinoza Lecture of 1999 from the European Association for Logic, Language and Information.

A solution to the problem of the classical interpretation of the Brouwer-Heyting-Kolmogorov semantics for propositional intuitionistic logic. This problem remained open since the papers by Kolmogorov (1932) and Goedel (1933, 1938) which informally specified intuitionistic logic via operations on proofs in classical mathematics. The solution of this problem given by proof polynomials is the one anticipated by Goedel in 1938.

1994-96. A logic based model of the references in data structures (joint papers with Krupski). A complete system of axioms describing references has been found. Algorithms synthesizing a reference data structure were suggested. This theory of references has been studied by the the Cornell PRL group pending applications in next generation automated deduction systems.

1987. A discovery of the modal logic A* which had completed the description of the class of modal counterparts of intuitionistic logic modulo well known Goedel’s translation (a Kuznetsov problem). The logic A* is now included to the list of the major modal logics (cf. A. Chagrov, M. Zakhar’yaschev, `Modal Logic‘, Oxford Logic Guides: v.35, 1997).

1985. A negative solution of the axiomatizability problem for the first order provability logic which was then the main problem in this area (cf. G. Boolos “The Logic of Provability”, American Mathematical Monthly, 91, pp. 470-480, 1984). A technique invented for this solution combined methods of proof theory and constructive models; it was later adapted by other researchers (Vardanyan, McGee, Boolos, Japaridze, Sidon) to study first order provability logics with limitations on a metatheory. This paper won the Best Paper of the Year award from the Steklov Mathematical Institute, the USSR Academy of Sciences in 1986.

1979. A uniform arithmetical completeness theorem for the modal logic of formal provability. This result considerably strengthened the Solovay completeness theorem and opened up a new line of research in provability logics (Visser, Japaridze, Beklemishev, Esakia, Shavrukov) which eventually led to a complete classification of all propositional modal logics of formal provability.

1978. A mathematical theory of optimal storage. Theoretical results were implemented in a system handling containers at sea port terminals. These results won the Best Project of the Year Award from the Optimal Control Institute of the USSR Academy of Sciences in 1979.