Roy Dyckhoff
Roy Dyckhoff 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 most well 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, Elisabeth Mary. His mother died on October 6, 1955, when he was only seven years old. Later remarrying in 1959, his father ran the law firm Dyckhoff and Johnson in Cheadle and founded the Cheadle Civic Society. Eric's collection of London and North Western Railway handbills and correspondences are kept at the John Rylands Research Institute and Library.Raised in Cheshire, he spent his youth at the prestigious boarding school Winchester College. As a student at Winchester College, Dyckhoff grew an interest in church bell-ringing, joining a group of ringers there. Roy spent a year programming punch-cards at English Electric Leo Marconi. 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. 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, he 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.