Remembering Roy Dyckhoff

摘要

Roy Dyckhoff left us after a long illness in August 2018. Many of us have known him as a teacher, colleague, mentor, friend, collaborator, and coauthor. He is much missed in the academic world, and especially in the Tableaux community, community, of which he was a founding father and an extremely active member. We shall remember Roy as a scientist with a broad range of interests, care for rigour, passionate approach to new ideas, and enthusiasm for new projects. He showed a human approach to scientific endeavour, had great care for acknowledging priorities, was generous in helping others and did not spare his personal involvement in easing conflicts and striving for justice. In his early years as a researcher, those of doctoral and postdoctoral study, Roy Dyckhoff gave substantial contributions to topology and category theory, the latter also studied in relation to Martin-Loef's type theory. Moving from mathematics to computer science he became interested in computational logic. In the early 1990s he started a systematic study of the use of sequent calculus as a basis for automated deduction, his most influential discovery being a terminating sequent calculus for intuitionistic propositional logic, known as G4 and published in 1992. He was not content with just any solution, but was always looking for the most elegant one. So he returned recently to this issue, improving the proof of the main result. Intuitionistic logic was a main thread of his research; to use his words, he surveyed "the wide range of proof systems proposed for intuitionistic logic, emphasising the differences and their design for different purposes, ranging from ease of philosophical or other semantic justification through programming language semantics to automated reasoning" as well as decision procedures and implementations thereof. In investigating the relationship between natural deduction and sequent calculus he settled an old problem on the relationship between cut elimination, substitution and normalisation. Furthermore, he studied the translations from intermediate logics to their modal companions as well as to the provability logic of Grzegorczyk logic, thus offering a fresh proof theoretic perspective on earlier semantical results. By his contributions relating sequent calculus and natural deduction he shed light on the connections between logic programming and functional programming, for instance regarding the concept of uniform proof. Roy Dyckhoff was appealed by the use of term rewriting techniques in proof theory, and explored innovative extensions of the Curry-Howard-De Bruijn correspondence, which relates formulae to types and proofs to functional programs. He contributed to the development of proof-term grammars and typing systems corresponding to various sequent calculi, with the notion of cut giving a natural typing rule for explicit substitutions, and with cut-elimination being expressed as terminating proof-term normalisation procedures. His contributions to this approach involve for instance the focussed sequent calculi LJT and LJQ, the sequent calculus G4, and Pure Type Systems. Roy Dyckhoff gave important contributions to the method of "axioms as rules"; in particular he proposed a view of rules as rewrite conditions and applied it to obtain a simple decision method, based on terminating proof search in a suitable sequent calculus, for the fragment of positively quantified formulas of the first-order theory of linearly ordered Heyting algebras. Recent work broadens the range of applications of the methodology of "axioms-as-rules." Not only many interesting mathematical theories can be expressed by means of coherent/geometric implications, classes of axioms that can be easily turned into rules, but any first order theory is amenable to such a treatment insofar it has a coherent conservative extension. Often classical conversion steps, such as those based on conjunctive and disjunctive normal form can (and should) be avoided. For this purpose, he devised a new algorithm of "coherentization" that preserves as much as possible of the formula structure. Roy Dyckhoff investigated proof theory also from the more general perspective of proof-theoretic semantics, in particular various notions of harmony, the question of what it is to be a logical constant, favouring the view that leads to strong normalisation results, and the relationship between general and "flattened" elimination rules. He also developed a proof-theoretic semantics for a fragment of natural language as an alternative to the traditional model-theoretic semantics. His scientific interests included systems of multimodal logics for encoding and reasoning about information and misinformation in multi-agent systems. For such logics he employed nested sequent calculi, a formalism beyond traditional Gentzen sequents and gave a Prolog implementation of a decision procedure. Roy Dyckhoff has always been fascinated by the challenge of understanding the classics by modern means, as he did for Frege's Begriffsschrift notation. More recently, he was engaged with Stoic logic. In he showed that the extension of the Hertz-Gentzen Systems of 1933 (without thinning) by a rule and certain Stoic axioms preserves analyticity, which in turn yields decidability of propositional Stoic logic. His latest publication shows how the rule of indirect proof, in the form with no multiple or vacuous discharges used by Aristotle, may be dispensed with, in a system comprising four basic rules of subalternation or conversion and six basic syllogisms. As is clear from this necessarily incomplete summary, Roy Dyckhoff had a proactive attitude that fostered collaboration. He always took genuine interest in the work of others. Many researchers across computer science, mathematics, and philosophy profited from his wide knowledge, deep insights and open-minded approach. He was exemplary in giving credit to others rather than claiming it for himself, and in setting high standards, while at the same time being gracious to those who did not meet them. His humility and his approach to academic life will continue to be an inspiration to all.