Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

Submitted by Richard Zach on Fri, 05/30/2014 - 5:46am

Very sad news today: Grisha Mints has died. He was born June 7, 1939 in Leningrad (now St. Petersburg). He received his education in mathematics at Leningrad State University under N. A. Shanin, and held positions there, at the Steklov Institute in Leningrad, and then, from 1980-1991, at the Estonian Academy of Science in Tallinn. In 1991 he joined the Philosophy Department at Stanford University, where he also held courtesy appointments in computer science and mathematics (since 1992 and 1997, respectively). In 2008 he was elected to the Estonian Academy of Sciences, and in 2010 named a fellow of the American Academy of Arts and Sciences.

Grisha was a force in logic, especially in proof theory. His early work centered on systems for automated theorem proving, where he contributed significantly to the development of Maslov's inverse method, resolution, and the relation between the two. He made major contributions to general proof theory, non-classical logics, constructive mathematics, program verification, and proof mining. He was the leading expert on Hilbert's epsilon calculus and the substitution method approach to the proof theory of strong subsystems of arithmetic. In addition to over 200 papers, he wrote two introductory books on modal and intuitionistic logic, and some of the early papers from his days in the Soviet Union were collected in his *Selected Papers in Proof Theory*.

I'm grateful to have had many beautiful interactions with Grisha over the years. The logicians at the TU Vienna had close contacts with Tallinn in the late 80's and early 90's, and I had the good fortune to meet Grisha then. While at Berkeley and Stanford, I attended a couple of his classes. He was a demanding teacher, but I learned a lot. I often visited before I taught at Stanford, and a few times since I've left. Whenever I did, he would ask me what I was working on, and he'd acknowledge what I'd said with a smile and a sideways nod and "um-hmm." Often he would then tell me about some obscure, usually Soviet-era, book or paper that addressed all the problems and questions I had. Then came the part where he'd tell me about his current work, and I would struggle to keep up. I'll always fondly remember those visits. He was a wonderful, generous teacher and colleague.

UPDATE: Memorial notice from Stanford's department chair Lanier Anderson.

- Kalmár's Compleness Proof
- Dana Scott's Favorite Completeness Proof
- Lectures on the Epsilon Calculus
- The Real Reasons Why Philosophers Shouldn't Use LaTeX
- Bringing Logic (and Philosophy, CS) to the Masses
- Proof Formalization in Mathematics: Guest Post by Jeremy Avigad
- Edward Nelson, 1932-2014
- Awodey's "HoTT for Philosophers" on mathtube.org

## Comments

This is very sad news indeed. During the year I spent at Stanford I had my office across the hall from Grisha, and no matter how early I arrived, he was already in his office, his door open, and would give me the sideways nod as he saw me come in. He was not only a great logician, but also a kind, warm person.

I would like to add a detail I heard directly from Grisha: Why was he in Estonia from 1980 on? Answer: He had applied for a permission to emigrate to Israel in the 1970s, permission denied. At the application, he was told that either he or his boss will be fired. He chose the latter, then somehow succeeded in getting a job in Estonia.

As to the latter, from http://www.cs.ut.ee/~varmo/tday-kaariku/GMe.pdf :

I am sorry for having missed what would have been the last chance to meet him, in a conference in St. Petersburg that I could not attend.

He was always enthusiastically engaged in listening to research ideas, giving advice and references, and spotting errors.

Two years ago in Oberwolfach I explained to him during a coffee break a result I had found (a generalised form of the first-order Barr theorem) and his immediate reaction was that it could not be correct. I knew that the result was correct because I had proved it, and the proof was very simple with the right method, yet he was absolutely sure it was wrong. Our discussion was interrupted by the beginning of the following talk. During that talk (not much followed by either of us, both mentally checking the proof) he turned repeatedly to my direction with a concerned expression. I had checked the result once more, so I knew why he was worried and why he was looking at me. He was afraid of having made me upset. In fact, during the next break, the first thing he told me was:

"Yes, you are right, it's correct!"

I'm not a proof-theorist, but during various conferences I had very frequent discussions with Grisha, he was often interested im my work. We eventually had a paper together, we finished it in late 2013, it should appear soon. It was a great pleasure to work with him

and to see his enthusiam!

Silvio

It is with deep sorrow that I learned of the death of Grigori

Mints. Over the past few years, I had a lot of contacts with him

being the organizer of the conference series "Philosophy,

Mathematics, Linguistics: Aspects of Interaction" held at the

Steklov Institute of Mathematics in St. Petersburg where Grigori

began his scientific career many years ago. I am grateful to him

for his participation as plenary speaker at these conferences in

2009, 2012, 2014. In the beginning of 2013, Grigori had readily

accepted our proposition to be the chairman of the Program Committee

of PhML-2014, which contributed so much to prepare the conference

program, particularly by involving all members of the Program

Committee in the process of discussion aimed to select papers for

presentation. Being the chairman of the Organizing Committee, I

conducted over this year an intensive e-mail correspondence with

him concerning a lot of subjects. Grigori had a plenty of ideas

and he expressed sincerely his opinion, which facilitated the

cooperation with him. He was generous to say good words about the

scientific achievements of his colleagues. Grigori was a bright

personality and he will be greatly missed to all who knew him.

In the end of 70s Grigori also made some very important contributions to Categorical Logic. One must mention his papers on proof theory in closed categories (there were two major papers, in 1977 and 1980, about coherence and natural deduction). I was his student in the end of 70s and wrote a diploma work under his supervision concerning coherence in Cartesian Closed Categories. The theme of my Ph.D. also was due to Mints, though he could not be (after 1980) my official supervisor and asked N.A. Shanin to take this role. I always remember with great admiration and emotion his open-mindedness, intellectual curiosity, honesty and generosity. In 70s and 80s he did in fact take part in the "dissident-style" seminars at S. Yu. Maslov's home, more a "free-thought" than "politics" place. Of course everybody there had access to "samizdat". The last time I have seen Grigori at St.-Petersburg in the end of this April at the PhML conference, where he seemed to be in good health. We had a discussion about proof-theoretical formalization of certain categorical notions, such as equalizers. Later the sad news were for me a complete shock.