University of Calgary
UofC Navigation

In Memoriam: Grigori Mints

LogBlog Has Moved!

You are looking at the old blog archive. LogBlog has moved to richardzach.org.
If you'd like to receive updates on new posts, please subscribe there!

Submitted by Richard Zach on Thu, 02/12/2015 - 10:59am

Grigori (“Grisha”) Mints died unexpectedly at Stanford on May 29, 2014. Born on June 7, 1939 in what is now St. Petersburg, Russia, Mints studied at the then Leningrad State University, obtaining a Masters degree in mathematics in 1961 with a thesis on proof search in classical predicate logic, a Ph.D. in 1965 with the thesis On Predicate and Operator Variants for Building Theories of Constructive Mathematics , and a D.Sc. in 1990 with Proof Transformations and Synthesis of Programs. From 1961 to 1979, Mints was a researcher at the Leningrad Branch of the Steklov Mathematics Institute. In 1980 he was appointed to a research position at the Institute of Cybernetics in Tallinn, Estonia. In 1991 he became a professor of philosophy and, by courtesy, of mathematics and computer science at Stanford University. Mints was elected to the Estonian Academy of Sciences in 2008 and to the American Academy of Arts and Sciences in 2010.

Mints’ research spanned several areas, with many interconnections. The grand unifying theme in his oeuvre was proof theory and constructivism, but entangled with this came a lifelong interest in computational logic as well as special attention for two specific areas: intuitionistic logic and modal logic.

Mints was trained in the Russian school of constructive mathematics of Markov and of his teacher Nikolai Shanin. In this paradigm, all mathematical objects should be defined in a finite language, and every proof of existence should provide an algorithm, where properties of the algorithm are to be proved by constructive principles including Markov’s schema. In tandem with this foundational view concerning mathematics, Shanin’s group at Steklov also worked on practical automated reasoning, with an emphasis on generating natural proofs, where ‘natural’ included making sense from the perspective of a human agent. This mixture of proof theory and computation led to inventions such as the inverse method, a style of analyzing provability similar to resolution, developed in 1964 by Sergei Maslov, a close friend of Mints.

Combining proof theory and computation naturally leads to a study of intuitionistic logic, and the most significant results of Mints’ first period concern this interface. They include an extension of Herbrand’s theorem to intuitionistic predicate logic (1962), and a proof of the undecidability of intuitionistic predicate logic with a single unary predicate (1965, a classical paper joint with Maslov and Orevkov). Some of these results are still under active investigation. Mints’ paper of 1968 on decidability of a certain fragment of the Gentzen system LJ introduced what is now called the “Mints hierarchy” of intuitionistic first-order formulas. Complexity properties of Mints classes are still under investigation (e.g., in recent works by Schubert, Urzyczyn, et al.), since they are important to understanding constructive type-theoretic proof assistants such as Coq. Also noteworthy is Mints’ proof in 1974 that familiar procedures for extracting programs from existence proofs in intuitionistic arithmetic produce equivalent algorithms.

In subsequent years, Mints turned to the study of relationships between proof theory and category theory. He used proof-theoretic methods to simplify proofs in category theory and to prove new theorems. Three key papers appeared in 19771980 in Russian (English translations in G. Mints, Selected Papers in Proof Theory, Bibliopolis and North-Holland, 1992). In particular, Mints gave a clear exposition of Lambek’s results connecting Cartesian closed categories and intuitionistic logic using a novel technique of encoding proofs as explicit proof-terms, an idea that has entered categorical logic itself, and that reemerged in modern manifestations such as Artemov’s justification logic. Important results obtained by Mints with this style of analysis include normalization and coherence theorems.

Mints retained his fundamental proof-theoretic interests throughout, witness his longstanding work on Hilbert’s epsilon calculus to subsystems of analysis right through his Stanford period.

During his stay in Estonia, Mints was actively involved with automated deduction. While in Tallinn, he studied the mathematical principles behind the program synthesizer PRIZ, designed by a group at the Institute of Cybernetics led by Enn Tyugu. Mints came up with an example that PRIZ could not handle, leading to an improvement of the algorithm for which Mints established completeness (1982, joint with Tyugu).

This applied work was based on Mints’ earlier research in proof theory for intuitionistic logic. But he also proved a large number of pure results in the area of intuitionism. These include his proof of Novikov’s hypothesis that a Tarski-style translation from Heyting arithmetic to modal arithmetic is faithful (1978). This result fits in an important line of system embeddings, whose later highlights include Flagg and Friedman (1984). Another long-standing interest of Mints in this area were interpolation theorems. An error in the interpolation proof by Lopez-Escobar for intuitionistic first-order logic with constant domains was found by him in 1983, and a recent joint paper with Olkhovikov and Urquhart (2012) finally produced a concrete and instructive counter-example. Mints’ book A Short Introduction to Intuitionistic Logic (2000) is a delightful introduction to the field with many original perspectives.

A natural step leads from intuitionism to modal logic. Mints was the first logician in the Soviet Union to work in modal logic, an exotic area in the 1960s. His first papers (1968-1969) addressed proof theory and decidability of first-order modal logics: in particular, he gave a cut-free sequent calculus for first-order S5 with equality. He also independently introduced the standard translation from modal to classical formulas, one of the main tools in contemporary modal logic. In 1974 he wrote an overview of modal logic in the period 1965-1973 including some of his own results (later transformed into the book A Short Introduction to Modal Logic, 1992).

In the 2000s, Mints proposed a study of basic laws of topology and of dynamical systems over these in a modal language. His results from this period include new proofs (some with Ting Zhang) of the completeness of S4 for the open unit interval and for Cantor space, and for the completeness of the basic dynamic topological logic S4C in Cantor space. Much of this work was collected in a chapter in the Handbook of Spatial Logics (2007), written by Mints and his collaborator Phil Kremer, which put this research program on the map. Recent new directions in his work included work on cut-elimination in fragments of the modal mu-calculus (2012).

Looking back at Mints’ work one sees a unity of themes and style that connected logic, mathematics, and computer science in many innovative ways. In addition he had a unique charm, formed by Russian and later on also by American culture, and a generous and encouraging intellectual attitude that exerted a strong positive influence on his colleagues, from America to Russia, and on successive generations of students until this very period. Many people owe him great ideas that set them on their paths, which he gave unstintingly, as well as help at crucial stages in their career.