Roy Dyckhoff

Roy Dyckhoff (4 March 1948 – 23 August 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 4 March 1948, in Manchester, to Eric Bernard Charles Dyckhoff, a solicitor, and Muriel Edith Turner. He had an older sister. His mother died on 6 October 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. During his time at King's College, he rang a peal at Trumpington with a band of first year students. 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. 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.

Personal life Dyckhoff married Cecilia Meredith in 1970, 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.