Fully funded PhD Studentship in Proof-theoretic Semantics at UCL
- Supervisors: David Pym (UCL CS and Philosophy), Elaine Pimentel (UCL CS), Tim Button
(UCL Philosophy)
- Research group: Programming Principles, Logic, and Verification (PPLV)
- Application deadline: 13:00 UK time (GMT) on 08 January 2024
- Supervisors' contact details (please use for informal discussions of the position):
Project Summary
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.
Non-classical, including substructural, logics are important classes of logics
that support more controlled reasoning than classical logic. They have found
significant academic and industrial application as the basis for tools for
reasoning about program and system correctness, where their ability to support
reasoning about the decomposition of structure is crucial in managing complexity
and scale, and in AI. The treatment of substructural and other non-classical
logics in P-tS, especially those of significance for agency, resource modelling,
and theories of information (e.g., relevance/modal/epistemic logics), requires
development.
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.
Candidates should have a Master’s degree in mathematics, philosophy, or
computer science and a strong interest in logic.