Roy Dyckhoff

Roy Dyckhoff (4 de marzo de 1948 - 23 de agosto de 2018) fue un matemático , lógico e informático británico que trabajó en lógica y teoría de la demostración en el Departamento de Matemáticas Puras y posteriormente en Ciencias de la Computación de la Universidad de St Andrews . ^{[ 2 ]} Es conocido por su descubrimiento en 1992 de un cálculo de secuencias terminantes para la lógica proposicional intuicionista . ^{[ 3 ] [ 4 ]} Su número de Erdős fue 3. ^{[ 5 ]}

Roy Dyckhoff nació el 4 de marzo de 1948 en Manchester , hijo de Eric Bernard Charles Dyckhoff, abogado, y Muriel Edith Turner. Tenía una hermana mayor. ^{[ 6 ]} Su madre falleció el 6 de octubre de 1955, cuando él tenía siete años. Posteriormente, se volvió a casar en 1959, ^{[ 7 ]} su padre dirigió el bufete de abogados Dyckhoff and Johnson en Cheadle y fundó la Sociedad Cívica de Cheadle. ^{[ 8 ]}

Criado en Cheshire , pasó su juventud en el internado Winchester College . ^{[ 9 ]} Dyckhoff desarrolló un interés por el toque de campanas de iglesia , uniéndose a un grupo de campaneros allí. ^{[ 10 ]} Dyckhoff pasó un año programando tarjetas perforadas en English Electric Leo Marconi . ^{[ 2 ]} Se matriculó en un programa de pregrado en King's College, Cambridge en 1966, estudió matemáticas pero también pasó un año asistiendo solo a clases de estudios de Oriente Medio . ^{[ 11 ]} Durante su tiempo en King's College, tocó un repique en Trumpington con un grupo de estudiantes de primer año. ^{[ 10 ]}

Tras obtener su licenciatura, continuó sus estudios en New College, Oxford , donde se doctoró en Matemáticas en 1974. Su tesis, titulada « Temas de topología general: bicategorías, recubrimientos proyectivos, aplicaciones perfectas y resoluciones de haces », fue dirigida por Peter J. Collins y Dana Scott . ^{[ 1 ]} Posteriormente fue nombrado miembro del Magdalen College, Oxford . ^{[ 11 ]}

En 1975, Dyckhoff se convirtió en profesor del Departamento de Matemáticas Puras de St Andrews , y posteriormente se trasladó a Ciencias de la Computación en 1981 ^{[ 9 ]} debido a la reducción de fondos bajo el gobierno de Thatcher . ^{[ 11 ]} Al principio de su carrera científica, contribuyó a la topología y la teoría de categorías . ^{[ 1 ] [ 12 ]} Aplicando su experiencia en programación y su interés en la lógica formal, se dedicó a la informática teórica y la lógica, donde llegó a especializarse en teoría de la demostración y demostración automatizada de teoremas . ^{[ 11 ]}

Sus investigaciones sobre lógica intuicionista lo llevaron a descubrir el cálculo de secuencias intuicionistas sin contracción G4ip en 1992. ^{[ 3 ] [ 13 ]} Se sabía que la regla de contracción era problemática para las búsquedas de pruebas hacia atrás, ya que puede causar bucles no deseados. Al producir un cálculo sin contracción y demostrar la admisibilidad de la contracción, Dyckhoff proporcionó el primer cálculo de secuencias proposicionales intuicionistas terminante . Dicho cálculo fue anticipado en la década de 1950 por el fundador de la escuela soviética de teoría de juegos , Nikolai Vorobyov . El cálculo de Dyckhoff sentó las bases para los sistemas de prueba terminantes posteriores. ^{[ 14 ]} Además, resolvió una cuestión planteada por Georg Kreisel en 1971 sobre la relación entre eliminación de cortes, sustitución y normalización. Fue coautor de varios artículos con Sara Negri sobre temas que involucran lógicas intermedias y modales . ^{[ 11 ]}

Sus trabajos posteriores investigaron la lógica aristotélica y estoica . Junto con Susanne Bobzien, demostró la decidibilidad de las lógicas estoicas en un sistema Hertz- Gentzen . ^{[ 15 ]}

Dyckhoff se casó con Cecilia Meredith en 1970, ^{[ 11 ]} y la pareja pasó su tiempo entre St Andrews y Glengarry, Invergarry en las Tierras Altas escocesas . Tuvieron dos hijos: una hija, Livia, y un hijo. ^{[ 16 ] [ 17 ]} Como capitán de la torre en la Capilla de San Salvador , Dyckhoff tocaba las campanas para varios servicios, involucrando ocasionalmente a su esposa e hijos en el toque. ^{[ 18 ]} Participó en la instalación de campanas adicionales en 2003 y más tarde en 2010 para conmemorar la consagración de la capilla y la fundación de la universidad. ^{[ 10 ]} También era un ávido excursionista y campanero en su tiempo libre, y apoyaba a la Asociación de Refugios de Montaña . ^{[ 9 ]}

Dyckhoff murió el 23 de agosto de 2018 a causa de una leucemia mieloide aguda . ^{[ 11 ] [ 19 ]}