Jump to content

Roy Dyckhoff

Add links
From Wikipedia, the free encyclopedia
Roy Dyckhoff
Born(1948-03-04)March 4, 1948
DiedAugust 23, 2018(2018-08-23) (aged 70)
Alma materUniversity of Cambridge, (BSc)
University of Oxford (Dr. Phil., 1974)
Spouse
Cecilia Meredith
​
(m. 1970)​
Scientific career
FieldsMathematics, Logic, Proof theory
InstitutionsUniversity of St Andrews
Thesis Topics in General Topology: Bicategories, Projective Covers, Perfect Mappings and Resolutions of Sheaves  (1974)
Doctoral advisorPeter J. Collins
Dana Scott
Doctoral studentsMuffy Calder[1]

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]

Early life and education

[edit]

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]

Career

[edit]

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]

Personal life

[edit]

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]

Later life and death

[edit]

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]

References

[edit]
  1. ^ a b c Roy Dyckhoff at the Mathematics Genealogy Project
  2. ^ a b "Dr Roy Dyckhoff: A Eulogy". St Andrews Computer Science Blog. 13 November 2018. Retrieved 1 June 2025.
  3. ^ a b Dyckhoff, Roy (1992). "Contraction-free sequent calculi for intuitionistic logic". Journal of Symbolic Logic. 57 (3): 795–807. doi:10.2307/2275431. S2CID 30194066.
  4. ^ Anne Sjerp Troelstra; Helmut Schwichtenberg (2000). Basic proof theory (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1.
  5. ^ "Roy Dyckhoff's page at St Andrews". Archived from the original on 2015-05-15. Retrieved 1 June 2025.
  6. ^ "Deaths, Dyckhoff". The Times. No. 66356. London. 11 November 1998. col Personal Column, p. 22.: "DYCKHOFF - Eric Bernard Charles, Solicitor, of Cheadle, Cheshire. Died peacefully on November 8th. 1998 after a short illness. Widower of Muriel and Jean and loving father of Elisabeth and Roy. Father-in-law of Cecillia, and grandfather of Livia and Max."
  7. ^ "Marriage 1938 - Eric Dyckhoff & Turner". FreeBMD. ONS. Retrieved 3 June 2025.
    "Death 1955 - Muriel Dyckhoff". FreeBMD. ONS. Retrieved 3 June 2025.
    "Marriage 1959 - Eric Dyckhoff & Wilson". FreeBMD. ONS. Retrieved 2 June 2025.
  8. ^ "About Us". Cheadle Civic Society. Retrieved 2 June 2025.
  9. ^ "Eric Dyckhoff collection". The John Rylands University Library - The University of Manchester. Archived from the original on 2008-05-09. Retrieved 2 June 2025.
  10. ^ a b c "Dr Roy Dyckhoff". St Andrews Computer Science Blog. 4 September 2018. Retrieved 1 June 2025.
  11. ^ a b c d Peter Williamson. "Obituary Roy Dyckhoff". Scottish Association of Change Ringers. Retrieved 1 June 2025.
  12. ^ a b c d e f g h "Annual Report 2019" (PDF). King’s College, Cambridge. Retrieved 1 June 2025.
  13. ^ Dyckhoff, Roy; Tholen, Walter (1987). "Exponentiable morphisms, partial products and pullback complements". Journal of Pure and Applied Algebra. 49 (1–2): 103–116. doi:10.1016/0022-4049(87)90124-1.
  14. ^ Graham-Lengrand, Stephane; Negri, Sara (2019). "Remembering Roy Dyckhoff" (PDF). Automated Reasoning with Analytic Tableaux and Related Methods. 28th International Conference, TABLEAUX 2019. London, UK. pp. xiv--xvii. doi:10.1007/978-3-030-29026-9.
  15. ^ Iemhoff, Rosalie (2022). "The G4i Analogue of a G3i Sequent Calculus". Studia Logica. 110: 1493–1506. doi:10.1007/s11225-022-10008-3.
  16. ^ Dyckhoff, Roy; Bobzien, Susanne (2019). "Analyticity, Balance and Non-admissibility of Cut in Stoic Logic". Studia Logica. 107: 375–397. doi:10.1007/s11225-018-9797-5. hdl:10023/13269.
  17. ^ "Roy Dyckhoff's page at the Department of Computer Science at St Andrews". Archived from the original on 2008-05-18. Retrieved 2 June 2025.
  18. ^ Clive Thompson (27 September 2007). "Smart Tweaks Amp Up Halo 3's Killer AI". Wired.
  19. ^ "2014 Annual Report" (PDF). Scottish Association of Change Ringers. Retrieved 2 June 2025.
  20. ^ "ASL Newsletter - January 2019" (PDF). Association for Symbolic Logic. Retrieved 2 June 2025.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Roy_Dyckhoff&oldid=1294739978"