Speaker:
Prof. Jonathan Seldin, University of Lethbridge, Canada

Abstract:
In this talk it is shown that every intermediate logic obtained from intuitionistic logic by adding a disjunction can be normalized. However, the normalisation procedure is not as complete as that for intuitionistic and minimal logic because some results which usually follow from normalisation fail, including the separation property and the subformula property.

Biography:
Jonathan P. Seldin, now Professor Emeritus, is a well-established senior scientist at the University of Lethbridge, Alberta, Canada, with an Amsterdam PhD in combinatory logic supervised by Haskell Curry. This logic, together with lambda-calculus (to which it is equivalent) is a prototype for functional languages, such as Haskell, and typed lambda-calculus is a prototype for the typing discipline in programming languages. His work on lambda-calculus, both pure and typed, has applications in formal verification, the use of formal logics to prove properties of programs (e.g., that they satisfy their specifications). He has co-authored works with Curry and Hindley on combinatory logic and lambda calculus. He is also interested in the history and philosophy of mathematics and in proof normalisation and cut-elimination for various systems of formal logic. His visit to Scotland is as a SICSA Distinguished Visiting Fellow, to work with Prof. Kamareddine at Heriot-Watt University and with Dr Dyckhoff at St Andrews. For details and publications see http://directory.uleth.ca/users/jonathan.seldin