Sergei Soloviev
email: soloviev@irit.fr

Grigori Mints, a Proof Theorist in the USSR: Some Personal Recollections in a Scientific Context

Keywords: Grigori Mints, Biography, Logic in the USSR, History of Logic

The paper is based on my recollections of Grigori Mints (1939Mints ( -2014) ) completed by a survey of his research work in a scientific context. I speak mostly about the Soviet period of his life and work (until 1991), and sometimes go beyond the purely scientific aspects to show the atmosphere of these times.

1

I first met Grigori when I was a second-year undergraduate at the Faculty 1 of Mathematics and Mechanics of Leningrad State University at the end of 1975 or in the beginning of 1976 2 . In the middle of our third year, we had to choose our specialization, and I had been considering mathematical logic as an option; simultaneously, I had been working on a project on uniform contact schemas under the supervision of N. K. Kossovsky, but I was attracted to the more theoretical aspects of logic. I had an acquaintance, Michael Gelfond, who was one of my teachers at the school N o 30 (a high school specialized in mathematics). He also was an associate of the Group of Mathematical Logic at the Leningrad Department of Mathematical Institute of the Academy of Sciences (usually called LOMI), where he defended his PhD thesis in 1974 3 . Gelfond advised me to go to the seminar of the Group of Mathematical Logic that was held at LOMI on Mondays, and to approach Mints.

I do not remember, whether I had to call Mints before and get an appointment. To enter LOMI I had to say that I go to the seminar because it was open to the colleagues of other institutes. To Mints I had to mention Gelfond's recommendation. In any case, when I approached Mints he suggested me to take the Russian translation of S. C. Kleene's "Mathematical Logic" [START_REF] Kleene | Mathematical Logic[END_REF], the so called "Red Kleene" 4 , and solve all the exercises. In fact, I never solved all of them because after some time, when I solved approximately one third (taken from all chapters), we had a much more lengthy and substantial discussion, and Mints proposed me to think about some original problems that were not merely exercises.

At this time he was much interested by some applications of proof theory to the theory of categories. It was Jim Lambek who first noticed the link between categories with additional structure and deductive systems. He published a series of three papers called "Deductive systems and categories" [START_REF] Lambek | Deductive systems and categories 1[END_REF][START_REF] Lambek | Deductive systems and categories 2[END_REF][START_REF] Lambek | Deductive systems and categories 3[END_REF]. Let me mention that two of these papers appeared in Springer Lecture Notes in Mathematics and were accessible in the LOMI's scientific library. Mints knew also about S. Mac Lane's works on coherence, but as far as I remember, most of all his attention was attracted by the recent paper by Mann [START_REF] Mann | The connection between equivalence of proofs and cartesian closed categories[END_REF] on the connection between the equivalence of proofs and the equality of morphisms in Cartesian Closed Categories probably because (in difference from Lambek) it considered natural deductions that were well known to Mints. This connection opened an interesting perspective in that certain problems of category theory, first of all the so called coherence problems (problems of commutativity of diagrams) may have nice proof-theoretical solutions.

In this essay I will try to render my impression of the style of Grigori Mints as a researcher. He was always very open, receptive towards the newest tendencies in all domains of world science related to proof theory and logic. Of course my impressions are subjective, and alone they cannot give a true idea of the whole extent and significance of his works, but I will try to complete this subjective part by a more academic survey based on publications, documents, and testimonies of G. E. Mints colleagues and friends.

Among the events that impressed me at this early period of my acquaintance with Mints was the visit (and talk) of an outstanding logician, G. Kreisel (1923Kreisel ( -2015) ) to LOMI in June 1976 that Mints organized.

The weather was unusually cold, but the central heating was already switched off because it was June.

At this time the building that LOMI occupied today 5 was under renovation and the institute was temporarily "exiled" to a former school far from the city center. It stood in an inner courtyard surrounded by gray buildings heavily styled since they were built in Stalin's times. Understandably, the conditions were more crowded. The group of mathematical logicians used a former classroom, and the seminars were held in the same room. I remember several tables, chairs, and a large worn leather divan, an object of amused pride in the group. Kreisel had to use an ordinary school blackboard for his talk. I also recall his coat, that seemed to me to be too light for such cold weather. Later I learned that these light coats protected against cold and rain much better than those "Made in USSR"'.

At that time I hardly asked myself what role Kresiel had played in the development of Mints as a scientist. I had no idea of the intense correspondence that Mints had with western scientists, often in spite of the obstacles and complexities typical of life in the USSR. Later I have heard from Mints that he considered Kreisel as one of his teachers 6 . He corresponded with many other Western scientists as well, for example, with A. S. Troelstra (b. 1939), S. Feferman (b. 1928), S. Mac Lane (1909[START_REF] Lane | A Mathematical Autobiography[END_REF]. In the archive of A. S. Troelstra first mention of the correspondence with G. E. Mints may be found in 1970 7 .

To give a better impression of "l'air du temps", it is worth to mention that the fact of correspondence with the West did not seem strange to me at all -the idea that science is indivisible, and the borders should not be an obstacle for scientific exchanges, was common among academic researchers and the university people at this time. The academic community in the USSR remembered very well that before the Revolution of 1917 and even in 1920s scientists easily published papers and exchanged letters in all main European languages (cf. [START_REF] Kh | On the History of Logic in Russia Before Revolution: Strategies of Academic Interaction[END_REF]), and did not want the return of Stalin's times.

Not long after my acquaintance with Mints I was invited to visit him at home -of course in connection with the problems he wanted to propose. A modest flat in one of the many areas of recent housing development, rather far (about 30 min. by tram or bus) from underground stations. Grigori lived there with his wife and daughter. I remember an impressive mathematical library -yellow spines of Springer Lecture Notes in Mathematics, foreign journals...

The third year at the University (in my case 1976/77) was the year of specialization, the scientific domain for the future graduation had to be chosen. I was included in the group of geometry and mathematical logics. The University administration agreed that Mints, who did not work at the University, would become my scientific adviser, and later supervisor of my graduate work. About these years, from 1977 to 1980, it is worth to speak in more detail.

The main problem that Mints proposed me to consider was the so called coherence problem for Cartesian Closed Categories. In proof-theoretical formulation, I had to prove that all logical derivations of certain classes are equivalent.

There were also lesser problems, that later turned out to be of independent interest, for example, the problem of transformations of derivations that preserved their equivalence. Mints suggested to read an old paper (1953) by G. F. Rose [START_REF] Rose | Propositional Calculus and Realizability[END_REF] where an interesting transformation of formulas (the decreasing of implicative depth) was considered, and to generalize it to the derivations. It required to go to the library of LOMI and make a considerable effort with English that I did not yet know well, but the paper was there and the effort within the limits of possible.

Georg Kreisel clearly distinguished what he called the "General Proof Theory" and the "Theory of Proofs" [START_REF] Kreisel | Some Facts from the Theory of Proofs and some Fictions from General Proof Theory[END_REF]:

A working definition of Proof Theory is essentially interested in what is traditionally called the essence or, equivalently, 'defining property' of proofs, namely their being valid arguments... general proof theory develops such refinements as the distinction between different kinds of validity, for example, logical or constructive validity (and other) familiar from the foundational literature... In contrast, the Theory of Proofs questions the utility of these distinctions compared to taking for granted the validity at least of currently used principles. Instead, this theory studies such structural features as the length of proofs and especially relations between proofs and other things, so to speak, 'the role of proofs'... As far as I know, Mints shared his views, and his own works mostly belong to the theory of proofs in Kreisel's sense. His interest in Categorical Logic, where logical derivations are seen as morphisms in appropriate categories, and equivalence relations on derivations generated by categorical semantics are studied, is in line with this approach.

In this period Mints wrote two long papers [START_REF] Mints | Theoretical applications of methods of mathematical logic[END_REF][START_REF] Mints | The theory of categories and the theory of proofs. Aktualnye problemy logiki i metodologii nauki. Kiev[END_REF], that considered the correspondence between certain systems of propositional logic and categories with additional structure. Main results included a solution of the "word problem" (equality of morphisms) in free categories with additional structure of several types: closed, symmetric closed, monoidal closed, symmetric monoidal closed, and cartesian closed, in all cases based on verification of the equivalence of derivations. As the main tool, the normalization of lambda-terms associated with derivations was used. Normalization at this time was relatively well explored by proof theorists, but its use for accurate and extensive study of categorical properties of proofs was new. Mints knew about a work of Mann [START_REF] Mann | The connection between equivalence of proofs and cartesian closed categories[END_REF] who used normalization for partial characterization of morphisms in Cartesian Closed Categories, and wanted to complete and extend his approach. Mints knew also about works of Lambek [START_REF] Lambek | Deductive systems and categories 1[END_REF][START_REF] Lambek | Deductive systems and categories 2[END_REF][START_REF] Lambek | Deductive systems and categories 3[END_REF] and Kelly-Mac Lane [START_REF] Kelly | Coherence in Closed Categories[END_REF], who with some success used cut-elimination 8 . Some of the systems considered by Mints correspond to what is called nowadays, after Girard's work [START_REF] Girard | Linear Logic[END_REF], multiplicative linear logic. In his paper [START_REF] Mints | Cut-elimination theorem for relevant logics[END_REF], 10 years before Girard, Mints cited several papers by Anderson and Belnap (e.g., [START_REF] Anderson | The pure calculus of entailment[END_REF]), Kreisel [START_REF] Kreisel | A survey of proof theory II[END_REF], and Prawitz [START_REF] Prawitz | Natural Deduction[END_REF]. Some indirect influence of Lambek [START_REF] Lambek | On the calculus of syntactic types[END_REF] may be possible.

One of two papers, published in Kiev [START_REF] Mints | The theory of categories and the theory of proofs. Aktualnye problemy logiki i metodologii nauki. Kiev[END_REF], was hard to find, and Mints gave me the manuscript to read.

At this period, when I wrote under Mints' direction my diploma work, he had also one PhD student, Ali Babayev. His story had some flavour of mathematical romantics. I mention it, because it shows Mints as an attentive and caring supervisor. Ali was first sent from Azerbaïdjan to Moscow for an internship under supervision of a prominent algebraist and logician Sergei Adian, but it did not go very well, and Ali felt himself somewhat lost. Mints met him during a visit to Moscow and invited to LOMI, to try to do a PhD thesis there under his own supervision. One of the problems that Mints suggested to Ali was identical to my own -he had to look for a proof of the so called coherence theorem for canonical morphisms in Cartesian Closed Categories, but we had to use different methods (Ali -lambda-calculus and natural deduction, and myself -Gentzen sequent calculus). Of course, Ali, as a PhD student had to work on several other problems. He had to explore other kinds of Closed Categories, for example, the so called Biclosed Categories, and related coherence problems. In the end we proved the coherence theorem for Cartesian Closed Categories more or less simultaneously.

Main results of this period of my work under direction of G. E. Mints were published in three papers in the volume 88 of "Zapiski" (1979). A long paper on coherence theorem contained two independent proofs, one obtained by Ali and another by myself [START_REF] Babayev | Coherence theorem for canonical maps in cartesian closed categories[END_REF]. Another paper [START_REF] Solov'ev | Preservation of equivalence of derivations under reduction of depth of formulas[END_REF] considered the preservation of equivalence of derivations under reduction of formula's depth by Rose's method. The third [START_REF] Solov'ev | Growth of the length of sequential derivation transformed into natural one[END_REF], a note of 3 pages, presented an example of exponential growth of length of natural deductions that correspond in a standard way to the sequential ones.

Mints published in the same volume two papers about various normalization problems concerning the arithmetical deductions and deductions in predicate calculus [START_REF] Mints | A new reduction sequence for arithmetic[END_REF][START_REF] Mints | A primitive recursive bound of strong normalization for predicate calculus[END_REF]. To me and Ali -the younger generation -it was difficult to figure out that for him a long and a very fruitful period of relatively peaceful creative work will soon come to an end.

2

All personal recollections have only limited meaning if they are not presented in a larger context, based on documents and information gathered from other people. This section is mostly devoted to an outline of such a more objective context.

Grigori Efroimovich Mints was born in Leningrad on June 7, 1939. The names of his parents were Efroim Borukhovich Mints and Lea Mendelevna Novik.

A few more biographical details. During the war, the family was evacuated and afterwards returned to Leningrad. In 1946 Grigori entered the school N o 241 at Oktyabrski district of the city of Leningrad. As an overwhelming majority in his generation, at the age of 14 he was enrolled to "Komsomol" (the union of communist youth). Of course, at this period of Soviet history for most of its members "Komsomol" was no more a bridge to the career in communist party, but mere formality. He finished school in 1956 and in the same year passed the exams and entered the Faculty of Mathematics and Mechanics of Leningrad State University, together with other future members of the Group of Mathematical Logic, S. Yu. Maslov (1939Maslov ( -1982) ) and G. V. Davydov. At the same time their future wives were enrolled.

Mints was taken to the section of computational mathematics 9 , that had at this time a "mixed" reputation in comparison with pure mathematics. On the one hand, the students of this section were considered as an elite of a sort, one had to have the very good marks at the entrance exams, at the other there was a risk because the graduates often were send to the institutes that worked on secret military projects, the so called "postboxes", since their street addresses were not publicly known. Remember that Soviet nuclear and space programs had at this time their "golden era", and they needed enormous amount of computations. By the way, it was also a refuge for cybernetics, that was not approved by Marxist philosophers, but they had no access to projects that had military significance. For a former student go to a "postbox" meant that it will be difficult to communicate with colleagues outside, and impossible to have contacts abroad. Happily for Mints and his friends, about 1956 the situation started to relax, and this permitted Mints, Maslov, and Davydov to be recruited immediately after graduation by LOMI, and become first junior members of the Group of Mathematical Logic just organized there under the leadership of one of the creators of constructive approach in mathematics, N. A. Shanin (cf. [START_REF] Yu | Nikolai Aleksandrovich Shanin (on his sixtieth birthday)[END_REF]).

In the end of 1960/61 academic year Mints defended his dimploma's work under the title "An Algorithm for Proof-Search in the Classical Predicate Calculus", and was awarded the diploma "with excellence" in the specialty "mathematics". He was immediately recruited by LOMI, and had to begin his work there on August 1st. His initial position was that of a research assistant, and he remained at this post a bit more than one year.

In 1962 the first two scientific papers by Mints were published in "Doklady" of the Academy of Sciences of the USSR (DAN) [START_REF] Mints | An analogue of Herbrand theorem for constructive predicate calculus[END_REF][START_REF] Mints | On the differentiability predicate and the differentiation operator[END_REF].

In 1963 he was elected by the Academic Council of LOMI to the position of Junior Researcher.

It followed afterwards almost two decades of uninterrupted and very impressive progress. In 1979 the official report signed by the administration of LOMI when the candidature of G. E. Mints for the position of senior researcher was proposed to Academic Council mentions that he has 60 published research papers and 13 articles for Mathematical Encyclopedia, Encyclopedia of Cybernetics, and other editions of similar kind. Mints was a member of the Group of Mathematical Logic, and this group itself was a remarkable association of the very talented and highly motivated researchers. In particular, it was developed and programmed by this group one of the first algorithms for automated proof-search in propositional and predicate calculus. All members of the group participated in this project.

As we shall see, one may discern more or less clearly the stages when the new interests became manifest in Mints' published works. A "cumulative effect" is obvious, i.e., the intensive research work helps to master new subjects faster, and on a deeper level.

During first 3-4 years at LOMI, proof theory, which is to become later the center of G. E. Mints interests, seems not yet to take a central position. In 1963 the joint paper (with V. P. Orevkov) "A generalization of the theorems of V. I. Glivenko and G. Kreisel to a class of formulae of the predicate calculus" is published in DAN [START_REF] Mints | A generalization of the theorems of V.I. Glivenko and G. Kreisel to a class of formulae of the predicate calculus[END_REF]. The name of G. Kreisel, who played later a very important role in Mints' scientific development, first appears in this early publication. In 1964 a long (54 p.) paper "On predicate and operator variants of the formation of theories of constructive mathematics" was published in "Trudy" of the Steklov Institute of Mathematics [START_REF] Mints | On predicate and operator variants of the formation of the theories of constructive mathematics. Problems of the constructive direction in mathematics. Part 3, Collection of articles. To the 60th anniversary of Andrei Andreevich Markov[END_REF]. It contained main results of Mints' PhD ("candidate of sciences") thesis, defended in 1965.

Until the end of his work at LOMI Mints remained a junior research fellow. With other members of the Group of Mathematical Logic he often got "bonuses" (i.e., complements to salary) for successful research. Generally speaking, the position of a junior researcher for a "candidate of sciences" at this time was not something unusual, though if we take into account the high research activity, typical for Mints, it seems rather questionable. His promotion to the position of a senior research fellow was considered only in the last months before he resigned. I discuss this below.

In 1965 the "Nauka" editions published the joint work that partly reflected the collective efforts of Logic Group in the development of an algorithm for automated proof search [START_REF] Davydov | An Algorithm for a Machine Search of a Natural Logical deduction in Propositional Calculus[END_REF]. According to Mints annual reports, he participated in the development of the program modules that concerned classical propositional calculus, classical predicate calculus with functional symbols, and in programming of the module "extraction" of this algorithm. The program ran on one of the first Soviet computers "Ural".

After the defense of his "candidate nauk" (PhD) thesis the scope of G. E. Mints work quickly expanded. He got into problems related to the central themes of mathematical logic in the XXth century. At the same time it became clear that its core was certainly the theory of proofs.

A personal feature of his style was an intense work on translations and surveys, and detailed comments to these translations and papers written by other researchers, that often contained the original results.

For example, in 1967 the collection of translations that included classical works in proof theory (papers by Gentzen, Gödel, Kleene and others), called "Mathematical theory of logical inference" was published [START_REF]Mathematical Theory of Logical Inference[END_REF]. Mints translated there four papers and wrote the 39 pages appendix "Herbrand Theorem" [START_REF] Mints | Herbrand Theorem[END_REF]. It contains, in particular, his own results about admissibility of substitution of terms for terms, used to correct an error in Herbrand's proof.

The survey [START_REF] Maslov | Mechanical Proof-Search and the Theory of Logical Deduction in the USSR[END_REF] (a joint paper with S. Yu. Maslov and V. P. Orevkov) was first work by Mints to be published abroad.

He wrote several appendices to the Russian translation of Kleene's "Mathematical Logic" [START_REF] Kleene | Mathematical Logic[END_REF].

In 1974 he published a long paper on the modal logics "The Lewis System and the System T" as an appendix to the Russian translation of R. Feys' book on modal logic [START_REF] Mints | Lewis' systems and system T (a survey 1965-1973[END_REF].

An important survey [START_REF] Mints | Proof theory (arithmetic and analysis)[END_REF] was published in 1975.

The same year a long "educational" paper [START_REF] Kreisel | The use of abstract language in elementary metamathematics: some pedagogic examples[END_REF] (the already mentioned joint work with Kreisel and Simpson) was published in the Springer Lecture Notes.

He wrote several appendices on proof theory to the Russian translation of Bar-wise's "Handbook of Mathematical Logic" 10 .

Back to the 60es, among other works that illustrate the rapid thematic expansion of Mints' work, let me mention his papers on modal logic [START_REF] Mints | Embedding operations related to the S. Kripke's "semantics[END_REF], on Skolem's method of quantifier elimination [START_REF] Mints | The Skolem method in intuitionistic calculi[END_REF], on embedding operations [START_REF] Mints | On embedding operations[END_REF], and on admissible rules [START_REF] Mints | Admissible and derivable rules[END_REF]. His work on Skolem's method for constructive predicate calculus was presented at the ICM in Moscow in 1966. (The collective work on machine proof search was also presented there.)

Until the end of 60s the most important works of Mints were published in the Proceedings of Steklov Mathematical Institute (MIAN), and the short announcements of important results in "Doklady" of the Academy of Sciences (DAN). In the end of 60s the requirements for the papers to be published in the LOMI's own series, "Zapiski" were changed. The longer papers that contained the full proofs and a detailed analysis of the problems under consideration could be published.

The simplification of publishing process, according to my experience, in many cases may be stimulating for research. Since 1967, when the first volume of "Zapiski" devoted to logic (vol. 4) appeared, until the end of his work at LOMI, almost all major works written by Mints were published there.

The "Zapiski" in the 60s-80s represented, to my opinion, an interesting example of a balance between creative research work and the selection process for publication. The papers were accepted for publication only after a talk at the Logic Seminar. To be presented, the talk had to be approved, usually on the basis of the short abstract, by the senior members of the Logic Group11 . When the volume was prepared, the text was read by some colleagues who played the role of referees. It is clear, that with this method of selection the results strongly depend on the ethical and scientific level of a research collective, but if it is scientifically and ethically adequate then the efficiency may be much higher than with "blind" selection methods that are common nowadays and assume certain level of mutual distrust.

I shall not give below a detailed account of all Mints works of the years that follow, because they are too numerous to be considered in this paper, but outline the main directions of his research and speak about some of the most significant papers.

The main topics that attracted the attention of G. E. Mints when he worked at LOMI are roughly the following:

First of all, his interest to general problems of proof theory, such as cut elimination, normalization, behavior of quantifier rules (including Herbrand theorem), never disappeared. It may be said, that this interest was always present as a background or at a technical side even when the main theme was different.

Other topics were:

• Modal logic

• Derived and admissible rules

• Infinite derivations and arithmetic

• Substructural and categorical logics

• Theory of Hilbert's ε-symbol Modal logic. All Mints' works on modal logic concern certain proof-theoretical aspects of modal systems. For example, embedding operations considered in [START_REF] Mints | Embedding operations related to the S. Kripke's "semantics[END_REF] are the operations that transform the derivations of one system in the derivations of another. Some other Mints' papers of this period on modal logic: [START_REF] Mints | Cut-free calculi of the S5-type. Studies in constructive mathematics and mathematical logic[END_REF][START_REF] Mints | On semantics of modal logic. Studies in constructive mathematics and mathematical logic, Part III[END_REF][START_REF] Mints | Lewis' systems and system T (a survey 1965-1973[END_REF][START_REF] Mints | On Novikov's hypothesis. Modal and intensional logics[END_REF]. A connection with provability logics is to be noticed, e.g., in the beginning of the paper [START_REF] Mints | On semantics of modal logic. Studies in constructive mathematics and mathematical logic, Part III[END_REF] Mints says: "necessity ... is interpreted as provability in classical propositional calculus" 12 .

Derived and admissible rules. [START_REF] Mints | Admissible and derivable rules[END_REF][START_REF] Mints | Derivability of admissible rules. Studies in constructive mathematics and mathematical logic[END_REF]. These papers may be seen as important steps towards the works of V. Rybakov and others, who obtained the criteria of admissibility of inference rules in large classes of logics (see, e.g., [START_REF] Rybakov | Admissibility of Logical Inference Rules[END_REF]).

Infinite derivations and arithmetic. [START_REF] Mints | Exact estimates for provability of the rule of transfinite induction in initial parts of arithmetic[END_REF][START_REF] Mints | On E-theorems[END_REF][START_REF] Mints | Theoretical application of methods of mathematical logic[END_REF][START_REF] Mints | Finite investigation of infinite derivations[END_REF][START_REF] Mints | A new reduction sequence for arithmetic[END_REF][START_REF] Mints | A primitive recursive bound of strong normalization for predicate calculus[END_REF]. Probably the most cited is [START_REF] Mints | Finite investigation of infinite derivations[END_REF]. The approach proposed by Mints (to consider transfinite derivations but study them using finitistic means) turned out to be very fruitful for extraction of constructive content of classical proofs (see, e.g., the recent book [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF]).

Substructural and categorical logics. [START_REF] Mints | Cut-elimination theorem for relevant logics[END_REF][START_REF] Mints | Theoretical applications of methods of mathematical logic[END_REF][START_REF] Mints | The theory of categories and the theory of proofs. Aktualnye problemy logiki i metodologii nauki. Kiev[END_REF]. As Mints himself explained in the end of [START_REF] Mints | Theoretical applications of methods of mathematical logic[END_REF], his cut-elimination theorem for relevant logic [START_REF] Mints | Cut-elimination theorem for relevant logics[END_REF] provided the substantial part of the normalization proof for the system that he developed for symmetric monoidal closed categories in [START_REF] Mints | Theoretical applications of methods of mathematical logic[END_REF]. His use of proof theory in these papers is quite elegant. The reader may see three kinds of logical systems in interaction: Hilbert-style systems, Gentzen calculi, and natural deduction. They are used to represent and explore various aspects of categorical structures. It becomes clear that not just some isolated methods, but the approach of the theory of proofs "as a whole" has a deep affinity with the theory of categories with structure (closed, symmetric closed, monoidal closed, symmetric monoidal closed, cartesian closed categories etc.). No doubt, these works contributed greatly to the development of categorical logic in its proof-theoretical aspect. These works and their ideas are still "in circulation". Let us cite, for example, [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and Their Use in Mathematics[END_REF] and [START_REF] Troelstra | Basic Proof Theory[END_REF] (especially Ch. 8).

Theory of Hilbert's ǫ-symbol. Mints (with Smirnov [START_REF] Smirnov | Elimination des termes ε dans la logique intuitioniste[END_REF] and Dragalin [START_REF] Dragalin | Intuitionistic Logic and Hilbert's ε-symbol[END_REF]) initiated the research on ε-symbol in the USSR, though before 1979 he published only one work on this subject [START_REF] Mints | Heyting Predicate Calculus with Epsilon Symbol (Russian). Studies in constructive mathematics and mathematical logic[END_REF]. Mints continued to work actively on the theory of the ε-operator after 1979. His last papers on the ε-operator were [START_REF] Mints | Intuitionistic Existential Instantiation and Epsilon Symbol[END_REF][START_REF] Mints | Epsilon substitution for first-and second-order predicate logic[END_REF][START_REF] Mints | Intuitionistic Existential Instantiation and Epsilon Symbol[END_REF]. It is interesting to notice that [START_REF] Mints | Heyting Predicate Calculus with Epsilon Symbol (Russian). Studies in constructive mathematics and mathematical logic[END_REF] keeps its actuality, even now. Bruno Woltzenlogel Paleo who works actually on ε-operator (in collaboration with Giselle Reis) stressed its relevance in e-mail that he sent to me recently 13 .

As an attentive reader would notice, Mints edited some of the volumes of "Zapiski" cited above. He was an editor of several books translated from English (e.g. [START_REF] Kleene | Mathematical Logic[END_REF]) and himself translated from English and German. He wrote many articles on mathematical logic for the Mathematical Encyclopedia, the Encyclopedia of Cybernetics, and even for the Great Soviet Encyclopedia (third edition).

I mention this to give a better idea of his "multidirectional" activity. He was among regular participants of Sergey Maslov's seminar, also known as the seminar on the general theory of systems. According to the recollections of Inna Davydova14 the seminar started at 1967, and initially the meetings were organized at the Faculty of Mathematics and Mechanics of the university. Later the seminar moved to S. Maslov's home because of the administrative pressure (I had myself an opportunity to attend it in the end of the 70s -beginning of the 80s).

Mints himself wrote in the foreword to the English edition of [START_REF]Problems of Reducing the Exhaustive Search[END_REF]:

The intellectual influence of the Maslov family was not restricted, however, to their scientific achievements. Their home in Leningrad (now St. Petersburg) was a meeting place of a seminar where talks on social and scientific problems were presented. One has to feel the gravity of the ideological pressure of a totalitarian state to appreciate the importance of such a free forum. The emergence of such seminars seems to be characteristic of intellectual life under oppressive regimes: recall Zilsel's seminar in Vienna where Gödel presented in January 1938 his overview of possibilities for continuing Hilbert's program. Another forum for dissident thought in the USSR was provided by a samizdat (unofficially published) journal "Summa" edited by S. Maslov which was designed as a review journal for samizdat publications.

Among the speakers were, for example, the philologist Vyacheslav Ivanov, a Foreign Fellow of British Academy since 1977 and Academician of Russian Academy of Sciences since 2000, the geneticist Raissa Berg, cf. the Columbia University Archive 15 , the literary critic and memoirist Lidiya Ginzburg (cf. [START_REF] Ginzburg | Blockade Diary[END_REF]).

In 1982 Maslov died tragically in a car accident.

In May 1979 the administration of LOMI finally considered Mints as a candidate for promotion to the position of senior researcher. On May 3 Mints signed an official request to submit his application, and the director of LOMI, L. D. Faddeev, endorsed the request. The meeting of the Academic Council of LOMI that had to consider the candidature was prepared as usual. On May 10 a recommendation was signed by the chef of Logic Group, N. A. Shanin. On May 25 an official appreciation of Mints research activity was signed by "troika" (direction, party secretary, and trade-union secretary). On June 28 the Academic Council of LOMI voted in favor of Mints candidature: 0 "against", 17 "for" (all of the present) of 21 members.

I do not know exactly what happened afterwards, but on August 31 Mints submitted another request, to be discharged from his position from 8 October.

The reasons of this abrupt change are not completely clear. The vote of the Council of LOMI was not the last step, after all it was only the Leningrad Department of the Mathematical Institute in Moscow (MIAN). The decision had to be confirmed there, and only after that the director of LOMI might sign the appointment order. Usually the confirmation came more or less automatically, but not always.

According to V. P. Orevkov, the direction of MIAN suggested Mints to make a presentation before the Academic Counsil there, and this was unusual. The general situation in the Academy of Sciences did not look well, for example, there were some known cases of antisemitism, and in some of these cases the director of MIAN I. M. Vinogradov was involved (see, e.g., the following letter of the Academician S. P. Novikov to one of his colleagues: http://www.mi.ras.ru/~snovikov/pont. pdf). Mints might learn that his appointment will be blocked at MIAN. He also might be informed about some external pressure that would make the promotion virtually impossible (for example, due to his "too extensive" international contacts not approved by authorities).

He would not like to continue as a Junior Researcher in such a circumstance. At the same time he might be reasonably convinced that, due to the same international contacts, he will be able to find a good employment at one of the Western universities 16 .

All colleagues who knew Mints and with whom I had an opportunity to discuss the events of 1979 (in particular, at Mints' memorial conference in August 2015) agree, that Mints asked to be discharged on his own request from LOMI because he decided to emigrate and wanted to save from blame Shanin, who, as the chef of Logic Group, would be otherwise held "administratively responsible". It seems that the decision to emigrate was taken somewhere between June and August.

It was not possible to emigrate freely from the USSR at this time, and Mints could not know that his emigration request will be refused by the authorities.

3

If Mints remained at LOMI, he would certainly become my PhD adviser after I graduated in 1979. In reality it was no more possible. He discussed this question with Shanin, and Shanin agreed to take me as his PhD student. It turned out, though, that finally the theme of my PhD thesis (defended in 1984) was essentially inspired by my graduate work under Mints supervision.

Shanin helped me a lot as far as the presentation of my results was concerned, advised on formulations that must be satisfactory from constructive point of view, but did not intervene much in the content.

I had some opportunities to discuss mathematics with Mints. I remember him to discuss the "Algebra of Proofs" by Szabo [START_REF] Szabo | Algebra of Proofs[END_REF] and the problem that was called (I do not remember, already at this time or later) the Mac Lane's conjecture 17 . He advised me to write S. Mac Lane about my work. I did, and our correspondence continued until the mid-90es.

Among other situations, I remember a very unpleasant moment in autumn of 1981 when I was contacted by the KGB who wanted to "ask some questions". I had no courage to refuse and was met in a park by a KGB officer in civilian clothes who did just that: asked questions about correspondence with abroad, about Maslov's seminar ... I tried to tell nothing of importance, and in spite of his explicit request to tell nobody, I informed Mints, Maslov and Shanin about this situation, but otherwise I remember nothing in my behavior to be especially proud of. Luckily for me their interest dissolved after a couple more meetings, probably they did not have anything serious in store.

The first half of the 80s, were for Mints a "time of troubles". He submitted an emigration request to the authorities an got a refusal. He had problems to find a job.

Of course his scientific research never completely stopped. Maybe it is a right place to say that one of his most impressive traits was calm, but almost religious devotion to science, and he had to find possibilities to do what he considered as his duty in a new and much less friendly environment.

At the same time there was nothing fanatical in this devotion, there certainly remained place for social life and human relations. For example after the tragic death of Sergei Maslov in 1982, Maslov's daughter Elena and his widow Nina for many years could count on his unwavering friendship 18 .

He had some contracts for translation with "Mir" and "Nauka" editions and tried to keep a usual level of scientific activity due to intense work on translations in spite of all difficulties and without an appropriate institutional affiliation. In 1981 "Mir" published the translation of G. Kreisel's selected papers [START_REF] Kreisel | Investigations in Proof Theory[END_REF] where Mints translated about 90 percent of the book. In a short autobiographical note published in [START_REF] Mints | Intuitionistic Existential Instantiation and Epsilon Symbol[END_REF], for the period 1979-1985 the collaboration with "Mir" and "Nauka" publishing houses is mentioned. In 1983 the translations (with Mints as one of translators) of Barwise's "Handbook of mathematical logic" [START_REF] Barwise | Handbook of mathematical logic[END_REF] and Chang and Lee's "Symbolic Logic and Mechanical Theorem Proving" [START_REF] Ch | Symbolic Logic and Mechanical Theorem Proving[END_REF] were published. The A. P. Ershov's archive 19 contains the correspondence between Ershov and Mints about the project to translate H. Barendregt's "λ-calculus". This project finally was accepted, not without difficulties and delays, and the translation was published by "Mir" in 1985. Still, this sort of contracts could not give any stability, and would disappear if no adequate research position would be found. Some hope of improvement came from his new contacts with Enn Tyugu and other Estonian scientists. Due to these contacts Mints had temporary invitations to Tallinn Institute of Cybernetics. The papers [START_REF] Mints | A simplified consistency proof for arithmetic. (Russian, English summary)[END_REF][START_REF] Mints | Logical Foundations of Program Synthesis[END_REF][START_REF] Mints | Justifications of the Structural Synthesis of Programs[END_REF][START_REF] Volozh | Theorem proving with the aid of program synthesizer[END_REF] were published. In 1983 he was an editor, with Enn Tyugu, of [START_REF]Automated Synthesis of Programs[END_REF]. Joint papers [START_REF] Mints | Justification of Structural Synthesis of Programs[END_REF][START_REF] Mints | Structural Synthesis of Recursive Programs[END_REF] are written for this collection. He wrote also a contribution (with Enn Tyugu) [START_REF] Mints | Structural Synthesis and Non-Classical Logics[END_REF] to the proceedings of the IIIth Conference "Application of methods of mathematical logic" in Tallinn.

However, how far from natural his situation was, is illustrated by the fact that from September 1983 to April 1985 he worked as a Senior Researcher at a computing center in the institute called Lengipromyasomolprom, that belonged to a large "holding" of Leningrad meat-processing plants (one of economic experiments of the late Soviet period) 20 .

In 1984 Mints helped to invite Saunders Mac Lane, though he of course could not be his "host" officially. Mac Lane came with his wife Dorothy, who had to use a wheelchair. As Mac Lane wrote:

In September 1984 we made another successful trip with the wheelchair, this time to Moscow, Leningrad and Helsinki. The occasion was an international conference and analysis to celebrate the anniversary of the Steklov Institute, the mathematical institute of the Soviet Academy of Sciences. [23, p. 303] In Leningrad Mints himself was a principal "guide" to Saunders and Dorothy. By grace of him, I had an opportunity to meet Mac Lane and discuss mathematics. I remember also how all of us visited the Alexander Nevsky Monastery and its historical necropolis, where Leonard Euler was buried.

After the death of Brezhnev in November 1982 the USSR entered the period of rapid political changes, though it was difficult to see at the beginning how far the changes will go.

In a quick succession Andropov, and after his death Chernenko, took office of the Communist Party's General Secretary. Chernenko in his turn died in March 1985.

I remember the dinner after the defence of the PhD ("candidate nauk") thesis by Valentine Shehtman. Shehtman was from Moscow, but to organize his defence there was more difficult, the reasons being far from scientific. He had his viva at LOMI, and booked in advance for the evening a private room at Metropole restaurant, one of the oldest and most traditional in Leningrad. It happened that at the same time the period of mourning because of Chernenko's death was declared, and the restaurant was unusually quiet.

I remember this as a kind of photograph: Mints, Shanin, Slissenko, Shehtman, Orevkov, Matiyasevich, Sochylina (the only woman), Ruvim Gurevich 21 , all in rather somber costumes (pure coincidence, not related to official mourning), all without ties (not a coincidence -somebody joked then that Shanin took as his students only those who do not wear a tie). I remember also a general feeling that the times are changing. They truly did. modern "proof-assistants". The importance of proof theory in programming was rapidly increasing.

In a narrow, strictly technical sense, the SSP may seem today a relatively limited topic but the research and development of the SSP in the 80s and the 90s contributed a lot to the much greater domain called now formal methods in programming.

The research position in Tallinn that Mints finally got did not diminish the intensity of his work, but he certainly should feel a relief finding himself again a member of a highly motivated research group, and in a more adequate status than before. One may be not particularly interested in career-making, promotions and honors, but still feel sharply that your work is not properly appreciated.

At Mints' Memorial Conference in St. Petersburg, V. Lifshitz23 mentioned that Mints was sometimes nicknamed a "minister of information"24 . Estonia in Soviet times was in many ways closer to the West than the rest of the Soviet Union, including better possibilities of scientific exchange, and this also should look for him as an improvement.

In 1986 Estonia was the venue of the IVth All-Union conference "Application of methods of mathematical logic". Mints was one of its organizers, and edited (with P. Lorents) the proceedings [START_REF] Mints | IVth All-Union conference "Application of methods of mathematical logic[END_REF].

The trip to Tallinn by train from Leningrad took only 6 hours. Many Leningrad residents enjoyed the visits to Estonian capital, especially to its historical center, an almost intact medieval city. The previous, IIIrd conference "Applications of methods of mathematical logic" in 1983, happened on the mainland, we were staying at the Olympic village in the Tallinn neighbourhood called Pirita, and often visited the city center.

This time the organizers had a more exotic plan. Its mere possibility seems to be a sign of changing times. A modest cruise ship that belonged to the Estonian Maritime Rescue was somewhat contracted, and the participants went from Tallinn to the Saaremaa island (part of the Estonian SSR). We stayed on the ship, but the conference meetings were organized at the Kuressaare Castle, a former bishop's stronghold.

Since 1986, after a long pause, Mints' papers were again published in international journals, for example rapidly appeared [START_REF] Mints | Semantics of a Declarative Language[END_REF][START_REF] Mints | The Programming System PRIZ[END_REF][START_REF] Mints | The Completeness of Provable Realizability[END_REF][76][START_REF] Mints | Propositional Logic Programming and Priz System[END_REF].

In 1988 he was one of the organizers of COLOG-88, an international conference on computer science logic in Tallinn. With Per Martin-Löf he edited the proceedings of this conference [START_REF] Martin-Löf | COLOG-88 : International Conference on Computer Logic[END_REF]. He also published a long paper there [START_REF] Mints | Gentzen-type systems and resolution rules. Part I. Propositional logic[END_REF].

The early 80s were difficult years, and had some profound personal consequences for Mints. They marked the end of his first marriage, because his first family finally decided not to emigrate. Later, when he moved to Estonia, they remained in Leningrad, that since 1991 is again called St. Petersburg.

I remember my meeting with Grigori and his second wife, Marianna, in Tallinn. It was probably during COLOG-88 or in 1989. Before the fall of the USSR, I visited the Institute of Cybernetics a few more times. One evening Mints invited me to his home, a kind of studio in some academic residence, the type doctoral students or post-docs might have. As far as I remember, it was stuff with scientific literature. We had some tea there surrounded by the bookshelves.

Mints probably still had plans to emigrate, but they could not be definite. In 1989 he defended his Dr. Sci. thesis25 titled "Transformations of Proofs and Program Synthesis". The defense took place at the Leningrad State University on April 26, 1989. In November 1989, he was promoted to the position of leading (or principal) researcher at the Tallinn Institute of Cybernetics.

In 1987 the borders started to open, and we could now easily go to the places that would seem impossible a few years ago. In fact, in the summer 1989, I was able to attend the ASL Logic Colloquium in West Berlin, just three months before the fall of the Berlin Wall. In 1990 I visited Mac Lane at the University of Chicago, and attended the Logic Colloquium '90 in Helsinki.

Mints was one of the invited speakers at both the Logic Colloquium '89 and the Logic Colloquium '90. In Helsinki it was probably the last time we met each other as Soviet citizens.

He was now in his element, at ease as a member of the top-level international scientific community that does not think much about borders. Of course, nothing was definitely settled yet in the ordinary, more mundane aspects of a scientist's life.

Enn Tyugu remembers:

We visited Stanford for three months in spring of 1990. He was proposed to be a lecturer of logic instead of Barwise who took his sabbatical, I guess, in the same autumn. He impressed the Stanford people so much that he got the permanent professorship there, moved to Stanford and left our institute in August 1991. 26It seems symbolic that one of the Mints' last papers that Mints had published when the Soviet Union still existed was a survey on proof theory in the USSR [START_REF] Mints | Proof Theory in the USSR 1925-1969[END_REF].

I was never able to visit Mints when he worked at Stanford there (1991-2014), though I did see him many times on other occasions. Let this period be the subject of another paper.

The head of the Group of Mathematical Logic (and Gelfond's PhD adviser) was N. Shanin. Gelfond emigrated to the United States in 1978. He is now a professor of computer science at Texas Tech University.

The translation (in red cover) was published in 1973. The book was translated by Yu. A. Gastev. Mints was the editor of the translation.

Cut-elimination alone does not permit to define normal forms, and so is not enough to solve the problem of equivalence.

In 1957 another future logician, V. P. Orevkov, also entered mathematical faculty.

Russian translation of "Handbook" was published in 4 volumes, v. 4, "Proof Theory" with these appendices was published in 1982.

Here only science mattered, and in this sense Mints of course was one of senior members.

The connection between modal logic and provability logic is known since Gödel[START_REF] Gödel | Eine Interpretation des intuitionistishen Aussagenkalküls[END_REF], but Mints' work may be seen as one of the inspirations for future fundamental works on provability logic, for example, by Artemov[START_REF] Artemov | Explicit provability and constructive semantics[END_REF].

6 of October 2015.

See http://www.mathsoc.spb.ru/pers/maslov. Gennady Davydov and his wife Inna were friends and colleagues ofMints and Maslov.

I already mentioned M. Gelfond who emigrated in 1978. Another colleague of Mints, V. Lifschitz, who defended his thesis under Shanin's supervision in 1969, emigrated to the USA in 1976. Both very quickly found an employment. However I am not sure that I am able to list all possible reasons.

[START_REF] Kreisel | Some Facts from the Theory of Proofs and some Fictions from General Proof Theory[END_REF] The conjecture says that the category of vector spaces is a complete model w.r.t. the axiomatic theory of Symmetric Monoidal Closed Categories.

It is not only part of my personal recollections, see, e.g., the A. P. Ershov's archive, http: //ershov-arc.iis.nsk.su/archive/eaindex.asp, Mints to Ershov, letter of 17 Sept.

[START_REF] Lambek | On the calculus of syntactic types[END_REF] See http://ershov-arc.iis.nsk.su/archive/eaindex.asp

This is confirmed by a document preserved at Tallinn Institute of Cybernetics.

Not to be confused with Youri Gurevich. I knew Ruvim since my student years at the faculty of mathematics and mechanics. He was a gifted mathematician, his best known result concerns the so called Tarski High School Algebra Problem[START_REF] Gurevič | Equational theory of positive numbers with exponentiation is not finitely axiomatizable[END_REF]. He emigrated in 1987 and died prematurely in 1989.

Essentially, it is a form of automated synthesis of programs, based on intuitionistic propositional calculus.

Like Mints, he defended his PhD thesis at LOMI (with Shanin as adviser). He emigrated in 1976 and is now professor at the University of Texas at Austin.

By the way, Mints wrote reviews for "Zentralblatt", "Mathematical Reviews" etc. since 1973. The total number of his reviews in "Zentralblatt" database is now 474. About 150 were written when he worked in Estonia (and about 15 before).

The degree that still exists in Russia, and is considered to be higher than PhD It may be compared to state doctorate that existed in many European countries until recently, and to habilitation that exists now.

[START_REF] Yu | Nikolai Aleksandrovich Shanin (on his sixtieth birthday)[END_REF] E-mail to the author,March 24, 2016.

Acknowledgements. I am very grateful to Evgeny Dantsin, Vladimir Orevkov, Anatol Slissenko, and Enn Tyugu for their recollections, help and advice. I would also like to thank the administration of the St. Petersburg Department of Steklov Institute of Mathematics for the opportunity to see archive documents concerning Grigori Mints.

* Partially supported by the Government of the Russian Federation Grant 074-U01 awarded to the ITMO University, St. Petersburg, Russia (associated researcher).

Let me quote again Mac Lane who visited the USSR again in 1987 (this time Mac Lane went first to Moscow, then to Tbilisi in Georgia, to Leningrad and finally to Estonia, where Mints now worked):

We then made a special trip to Tbilisi, Georgia, which was then still part of Soviet Union. But discontent over the political system was in the air ... From Leningrad we continued to Estonia, where I gave a talk at the Institute of Cybernetics in Tallinn and we were again greeted warmly by colleagues, both in Tallinn and at the University of Tartu. In Estonia too, we were much aware of the limits of freedom of speech. However, only a few weeks later glasnost and big changes took place in the Soviet system. Amazing! Within a few days, Georgians, Russians, Estonians, all were now allowed to communicate without fear.( [START_REF] Lane | A Mathematical Autobiography[END_REF], p. 331.) Since April 1985 Mints was fully employed as a Senior Researcher at the Institute of Cybernetics of the Estonian Academy of Sciences in Tallinn. I have outlined in the previous section the main directions of his research in the 60s and the 70s. In the 80s his main contributions were certainly in the domain of computer science logic. He participated actively in a pioneering research on structural synthesis of programs (SSP), the proof-theoretical aspects of structural synthesis being mostly his responsibility 22 .

If we look today what came out of these studies then we shall see that some research still continues (see [START_REF] Tyugu | Grigori Mints and Computer Science[END_REF], and the bibliography there) but we may have an impression that the topic remains rather limited. In fact, it would be fair to take into account the historical context and the role of SSP in this context, because for proof theoretical methods in computer science the 80s were an early "heroic" period.

The attempts to use computers for proof search and verification started in the 60s, but the 70s and the 80s had seen the first steps to implement the idea that proofs themselves may have something to do with structuration and execution of programs. For example, the Prolog language, created in 1972 by A. Colmerauer and Ph. Roussel, was then a "hot topic" among proof theorists interested in applications. Another "hot topic" was the Curry-Howard correspondence [START_REF] Howard | The formulas-as-types notion of construction[END_REF].

In the 1970s R. Milner with his group created at Edinburgh university the ML programming language, based essentially on the principles of typed λ-calculus. In his paper on LCF (logic for computable functions) Milner wrote:"The connection between programs and logic is now recognized as a leading topic of research in the theory of computing." [START_REF] Milner | LCF: A Way of Doing Proofs with a Machine[END_REF], p.146. P. Martin-Löf was developing his Type Theory, that plays a central role in many