Roy Dyckhoff

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.^[2] He is most well known for his discovery in 1992 of a terminating sequent calculus for intuitionistic propositional logic.^[3][4] His Erdős number was 3.^[5]

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, Elisabeth Mary.^[6] His mother died on October 6, 1955, when he was only seven years old. Later remarrying in 1959,^[7] his father ran the law firm Dyckhoff and Johnson in Cheadle and founded the Cheadle Civic Society.^[8] Eric's collection of London and North Western Railway handbills and correspondences are kept at the John Rylands Research Institute and Library.^[9]

Raised in Cheshire, he spent his youth at the prestigious boarding school Winchester College.^[10] As a student at Winchester College, Dyckhoff grew an interest in church bell-ringing, joining a group of ringers there.^[11] Roy spent a year programming punch-cards at English Electric Leo Marconi.^[2] This experience convinced him to pursue a career in academia instead of industry. 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.^[12] During his time at King's College, he rang a peal at Trumpington with a band of first year students.^[11]

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.^[1] He was later appointed Fellow of Magdalen College, Oxford.^[12]

In 1975, he became a Lecturer in the Department of Pure Mathematics at St Andrews, later moving to Computer Science in 1981^[10] due to the reduced funding under the Thatcher government.^[12] Early in his scientific career, he contributed to topology and category theory.^[1][13] 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.^[12]

His investigations into intuitionistic logic led him to discover the contraction-free intuitionistic sequent calculus G4ip in 1992.^[3][14] 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.^[15] 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.^[12]

His later works investigated Aristotelian and Stoic logic. With Susanne Bobzien he proved the decidability of Stoic logics in a Hertz-Gentzen system.^[16]

Roy married Cecilia Meredith in 1970,^[12] 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, Max, who later went on to work as engineer for Bungie on Halo 3.^[17][18] As a Tower captain at the St Salvator's Chapel, Roy rang for various services, occasionally involving his wife and children in the ringing.^[19] 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.^[11] He was also an avid hiker and bell-ringer in his free time, and supported the Mountain Bothies Association.^[10]

Despite worsening health, Dyckhoff continued to support ringing at St Andrews and the Tulloch Ringing Centre in Roybridge.^[11] Roy Dyckhoff died on the morning of the 23rd of August 2018, aged 70, from an acute myeloid leukemia.^[12][20] He was survived by his daughter Livia and son Max Dyckhoff.^[12]