Roy Dyckhoff (March 4, 1948 – August 23, 2018) was a British mathematician, logician and computer scientist who worked in logic and proof theory in the Department of Pure Mathematics and later Computer Science at the University of St Andrews. He is known for his discovery in 1992 of a terminating sequent calculus for intuitionistic propositional logic. His Erdős number was 3.
Early life and education Roy Dyckhoff was born on March 4, 1948, in Manchester, to Eric Bernard Charles Dyckhoff, a solicitor, and Muriel Edith Turner. He had an older sister. His mother died on October 6, 1955, when he was seven years old. Later remarrying in 1959, his father ran the law firm Dyckhoff and Johnson in Cheadle and founded the Cheadle Civic Society. Raised in Cheshire, he spent his youth at boarding school Winchester College. Dyckhoff grew an interest in church bell-ringing, joining a group of ringers there. Dyckhoff spent a year programming punch-cards at English Electric Leo Marconi. Enrolling in an undergraduate program at King's College, Cambridge in 1966, he studied mathematics but also spent a year attending only lectures in Middle Eastern studies. During his time at King's College, he rang a peal at Trumpington with a band of first year students. After receiving his undergraduate degree, he pursued further studies at New College, Oxford, completing a DPhil in Mathematics in 1974. His dissertation, Topics in General Topology: Bicategories, Projective Covers, Perfect Mappings and Resolutions of Sheaves, was supervised by Peter J. Collins and Dana Scott. He was later appointed Fellow of Magdalen College, Oxford.
Career In 1975, Dyckhoff became a lecturer in the Department of Pure Mathematics at St Andrews, later moving to Computer Science in 1981 due to the reduced funding under the Thatcher government. Early in his scientific career, he contributed to topology and category theory. Applying his experience in programming and interest in formal logic, he shifted to theoretical computer science and logic where he came to specialise in proof theory and automated theorem proving. His investigations into intuitionistic logic led him to discover the contraction-free intuitionistic sequent calculus G4ip in 1992. The contraction rule was known to be problematic for backward proof-searches as it can cause unwanted loops. By producing a contraction-free calculus and proving the admissibility of contraction, Dyckhoff provided the first terminating intuitionistic propositional sequent calculus. Such a calculus was anticipated in 1950s by the founder of the Soviet school of game theory, Nikolai Vorobyov. Dyckhoff's calculus laid the groundwork for subsequent terminating proof systems. Additionally he settled a question posed by Georg Kreisel in 1971 on the relationship between cut-elimination, substitution and normalisation. He co-authored several papers with Sara Negri on topics involving intermediate and modal logics. His later works investigated Aristotelian and Stoic logic. With Susanne Bobzien he proved the decidability of Stoic logics in a Hertz-Gentzen system.
Personal life Dyckhoff married Cecilia Meredith in 1970, and the couple spent their time between St Andrews and Glengarry, Invergarry in the Scottish Highlands. They had two children: a daughter, Livia, and a son. As a Tower captain at the St Salvator's Chapel, Dyckhoff rang for various services, occasionally involving his wife and children in the ringing. He was involved in the installation of additional bells in 2003 and later in 2010 to commemorate the consecration of the chapel and the founding of the university. He was also an avid hiker and bell-ringer in his free time, and supported the Mountain Bothies Association. Dyckhoff died on 23 August 2018 from an acute myeloid leukemia.
References
