Propositional- and Predicate-Calculus Preliminaries


This chapter prepares for the extensive account of a proof-verification system based on set theory which will be given later. Two of the system’s basic ingredients are described and analyzed:
  • the propositional calculus, from which all necessary properties of the logical operations &, ∨, ¬, →, and ↔ are taken, and

  • the (first order) predicate calculus, which adds compound functional and predicate constructions and the two quantifiers ∀ and ∃ to the propositional mechanisms.

A gradual account of the proof of Gödel’s completeness theorem for predicate calculus is provided. Notions which are relevant for computational logic, such as reduction of sentences to prenex normal form, conservative extensions of a first-order theory, etc., are also introduced.

The Zermelo–Fraenkel set theory is introduced formally as an axiomatic extension of predicate calculus, and consistency issues related to it are highlighted.


Free Variable Propositional Calculus Function Symbol Predicate Calculus Predicate Symbol 


  1. [Jec97]
    Jech, T.J.: Set Theory, 2nd edn. Perspectives in Mathematical Logic. Springer, Berlin (1997) MATHGoogle Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

There are no affiliations available

Personalised recommendations