Computational Logic and Set Theory pp 3791  Cite as
Propositional and PredicateCalculus Preliminaries
Chapter
Abstract
This chapter prepares for the extensive account of a proofverification system based on set theory which will be given later. Two of the system’s basic ingredients are described and analyzed: 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 firstorder theory, etc., are also introduced.

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.
The Zermelo–Fraenkel set theory is introduced formally as an axiomatic extension of predicate calculus, and consistency issues related to it are highlighted.
Keywords
Free Variable Propositional Calculus Function Symbol Predicate Calculus Predicate SymbolReferences
 [Jec97]Jech, T.J.: Set Theory, 2nd edn. Perspectives in Mathematical Logic. Springer, Berlin (1997) MATHGoogle Scholar
Copyright information
© SpringerVerlag London Limited 2011