Adding metatheoretic facilities to first-order theories (Q2785674)

Generic proof systems (like the Isabelle logical framework) provide some limited but useful metatheoretic facilities for declared logics; in particular, users can prove simple derived rules and also `solve' formulae that contain metavariables --- a technique useful for, e.g., program synthesis. The authors explore these two kinds of metatheoretic extensibility, and their applications. Their contribution is to show that rather than using a system like Isabelle, these kinds of extensibility can be directly added to an arbitrary first-order theory by conservatively extending it with quantifiers over formulae, that is, without recourse to an independent metatheory. This can be seen as a proof-theoretic investigation into aspects of the metatheory of various generic proof systems and how they can be simulated in weak extensions of first-order theories.