Expressiveness and Complexity in Proof Systems (URSA PhD Project)

Project Overview: The Faculty of Science URSA PhD Project at the University of Bath offers an exciting opportunity to explore the expressiveness and complexity of proof systems, a foundational topic in mathematical logic, computer science, and formal reasoning. This project is part of the competitive URSA studentship scheme for entry in September 2026. Research Focus: Formal proofs are central to logic, mathematics, and computer science, underpinning everything from philosophical reasoning to automated verification. The project investigates how proof systems and their formalisms—such as sequent calculi, hypersequents, nested sequents, labelled calculi, and cyclic proofs—define the expressive and computational boundaries of logical reasoning. The aim is to develop a unified account of the expressive power and limitations of these formalisms, identifying structural principles that determine when logics admit properties like interpolation or the disjunction property, regardless of the calculus used. The research will build on recent advances to generalise methods across different proof frameworks. Candidate Profile: The ideal candidate will have a strong background in mathematics and a keen interest in mathematical logic. Experience in proof theory, non-classical logics, and related areas is highly desirable. Applicants should hold, or expect to receive, a First Class or good Upper Second Class UK Honours degree (or equivalent) in a relevant subject. A master’s qualification is advantageous. International applicants must meet the English language requirements by the application deadline. Funding: Candidates may be considered for a University of Bath studentship, tenable for 3.5 years. The studentship covers tuition fees, a generous stipend (£20,780 per annum for 2025/6), and access to a training support budget. While the studentship is open to both Home and exceptional International students, international applicants should note that relocation costs, visa fees, and the UK healthcare surcharge are not covered. Supervision: The project will be supervised by Dr Raheleh Jalali Keshavarz and Prof J Davenport, both experts in mathematical logic and proof theory. Informal enquiries are encouraged and should be directed to Dr Jalali Keshavarz. Application Process: Formal applications must be submitted via the University of Bath’s online application form for a PhD in Computer Science. Applicants should select ‘University of Bath URSA’ as the studentship and quote the project title and lead supervisor’s name in the relevant sections. Early application is recommended, as the position may close before the advertised deadline if a suitable candidate is found. Equality, Diversity and Inclusion: The University of Bath values diversity and encourages applications from under-represented groups. Applicants with circumstances affecting their educational attainment are invited to include a short paragraph in their personal statement. References and Further Reading: For more information on the research context, see the following references: - Universal Proof Theory, TACL 2022 Lecture Notes - Universal proof theory: Semi-analytic rules and Craig interpolation - Uniform interpolation and the existence of sequent calculi Institution: University of Bath, Department of Computer Science, United Kingdom. Deadline: 1 May 2026 (early application recommended).