Propositional non-classical logics extend classical propositional logic
(CPL) with further connectives to capture notions such a "necessarily
phi" or "possibly phi" or even "phi is provable in Peano Arithmetic".

Naturally, proof-calculi for non-classical logics extend those for
CPL. For example, Hilbert-calculi for non-classical logics incorporate
further axioms over the new connectives while Gentzen-calculi for these
logics utilise new rules of inference over the new
connectives. Gentzen-calculi in particular, involve a highly non-trivial
combinatorial proof of completeness which is mathematically intricate.

The aim of the project is for the student to become familiar with
various non-classical logics and their associated proof-calculi.
There is potential for the student to continue this line of research
into an honours project.