| Abstract: | The paper provides a uniform Gentzen-style proof-theoretic framework for various subsystems of classical predicate logic. In particular, predicate logics obtained by adopting van Behthem's modal perspective on first-order logic are considered. The Gentzen systems for these logics augment Belnap's display logic by introduction rules for the existential and the universal quantifier. These rules for  x and  x are analogous to the display introduction rules for the modal operators  and  and do not themselves allow the Barcan formula or its converse to be derived. En route from the minimal  modal predicate logic to full first-order logic, axiomatic extensions are captured by purely structural sequent rules. |
