Fully funded PhD Studentship in Proof-theoretic Semantics at UCL, Londen (UK)

Proof-theoretic semantics (P-tS) offers a practical foundation for the meaning of logical theories that is grounded inference — that is, reasoning — rather than the abstract structures of model theory. It lies within the philosophical position known as inferentialism. As such, P-tS offers an alternative foundation for mathematical logic that places reasoning at the heart of meaning. P-tS has two primary variants: Dummett-Prawitz validity, closely related to Brouwer-Heyting-Kolmogorov semantics, and base-extension semantics, which can be seen as bridge to model-theoretic semantics. Base-extension semantics will be the primary focus of this project, with the Dummett-Prawitz view also relevant.

This studentship (intersecting informatics, mathematics, philosophy) will address giving proof-theoretic semantics to non-classical logics, developing the necessary abstract mathematical meta-theory and exploring the significance of inferentialist semantics, and its mathematical realization, for systems verification. This latter aspect will build directly on connections between the proof-theoretic foundations of logic programming and base-extension semantics recently established at UCL. Connections to simulation modelling and its inferentialist interpretation may be explored.

The student will work with Prof. David Pym (Computer Science and Philosophy), Dr. Elaine Pimentel (Computer Science), and Prof. Tim Button (Philosophy), and be based in the Programming Principles, Logic, and Verification group.