Proofs and Algorithms Gilles Dowek (translation by Maribel Fernandez)

摘要

Chapter 1 is a lengthy presentation of predicate logic (with the definitions of language and term, the former being a set of sorts (types) and a set of typed relation and function symbols, and the latter, type-respecting compositions of symbols), the notions of sequent, proof (with natural deduction), and theory (with a few examples including Zermelo-Fraenkel set theory). A discussion is given on other ways to express the axiom of excluded middle, with, as an important step, the introduction of the so-called "System D'" (the name is not motivated), i.e., natural deduction with multiple conclusions. Chapter 2 presents the concept of model. Therein the soundness theorem (if a theory has a model, it is consistent) and the completeness theorem (if a theory is consistent, it has a model) are proved. Although Godel's second incompleteness theorem is deemed "out of scope" for the book, a quick presentation of relative consistency proofs is given. The notions of extension and preservation under extension are then presented, together with Skolem normal form. The chapter is closed with a weak form of Lowenheim-Skolem theorem.