Predicate Logics on Display

  • Heinrich Wansing
Part of the Trends in Logic book series (TREN, volume 3)


This chapter provides a uniform Gentzen-style proof-theoretic framework for various subsystems of classical predicate logic. In particular, predicate logics obtained by adopting van Benthem’s modal perspective on first-order logic are considered. The Gentzen systems for these logics augment Belnap’s display logic, DL 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. The chapter has two main aims, namely
  1. 1.

    presenting a uniform proof-theoretic schema for both substructural subsystems of classical first-order logic, FOL and various subsystems of FOL obtained by relaxing Tarski’s truth definition for the existential and universal quantifiers, and

  2. 2.

    introducing these quantifiers into the framework of DL.



Modal Logic Predicate Logic Structural Rule Sequent Calculus Axiom Schema 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1998

Authors and Affiliations

  • Heinrich Wansing
    • 1
  1. 1.Institute of Logic and Philosophy of ScienceUniversity of LeipzigLeipzigGermany

Personalised recommendations