Proof theory has a successful and mature history of describing proofs and their properties for first-order classical and intuitionistic logics. Mathematics and computer science, however, requires much more than is offered by these logics alone. For example, if one needs to formalize notions such as sets, algebras, and order relations, one can introduce theories to axiomatize the properties needed of these notions.
A more sophisticated treatment of axioms in a theory would be to convert them into inference rules. Recent work by Negri et. al. [NvP01, N05] and Ciabattoni et. al. [CGT08] have made progress in doing exactly that for a range of theory types.
The main goal of this internship is to discover the extent to which recent work in focused proof systems for classical and intuitionistic logics can be used as a general framework for converting axioms into inference rules.
Goal 1: Show how a range of common theory types (for example, Horn clauses and geometric theories) can be viewed as inference rules in which cut and initial both can be eliminated. Use the framework of focused proof systems in classical and intuitionistic logic [LM09] to prove these results. What limits to this method can you find?
There are several ways to judge whether or not one's treatment of axioms-as-rules is of ``high quality''. One such way involves applying that treatment to, say, modal logics. The semantics of such logics are usually given by classes of (Kripke) models in which the accessibility relationship is axiomatize by various theories.
Goal 2: Proof systems for modal logics can be made with or without explicit reference to possible worlds and the theories that define their accessibility relations. Use the results above to show how explicit codings can be abstracted away to yield the ``implicit'' proof system.
Goal 3: Show how an explicit proof representation for modal logic formulas (in both classical and intuitionistic logics) can be checked using proof checkers that do not have underlying modal operators.
This internship will take place within the funding context of the ProofCert project (an ERC Advanced Investigator Award). This five year project (2012-2016) provides funding for PhD students covering a broad range to topics in a foundational approach to proof certificates. Continuing to work on this topic for a PhD is possible and encouraged.
The following bibliography is indicative of the kind of papers that will be part of this research effort.