Proofs and algorithms. An introduction to logic and computability (Q625290)

Dowek's book (published in the series Undergraduate Topics in Computer Science and based on his course notes) deals with the relationship between proofs and algorithms as fundamental concepts of contemporary logic (and theoretical computer science). The book consists of three parts: Proofs; Algorithms; Proofs and algorithms. In the first part, basics of predicate logic and models are given. Chapter 1 brings a concept of inductive definitions (fixed-point techniques, structural definitions, languages with and without variables, many-sorted languages, predicate logic and its proofs, and examples of theories). Chapter 2 is devoted to models (basic definitions, soundness and completeness theorems, models of equality, consistency and relative consistency, extensions of theories and models). The second part starts with Chapter 3, which is devoted to computable functions (definition of computable function and proofs that some basic functions are computable, decidable and semi-decidable sets, a pairing function and computability over lists and trees, relation between functions and programs, undecidability of the halting problem, an interpreter as a universal computable function). The next chapter presents computation as a sequence of small steps (rewriting rules, redex, reduction step, relation between computable functions and sets of rewriting rules, the lambda calculus and its relation to computable functions, Turing machines and their relation to computable functions). The first chapter of the third part of the book (Chapter 5, Church's Theorem) gives basically the preparations for the main results: undecidability of arithmetic; Church's theorem of undecidability of languages with at least one binary predicate; semi-decidability of a theory with a decidable set of axioms; Gödel's first incompleteness theorem. Chapter 6 (Automated theorem proving) deals with different proof techniques: sequent calculus and natural deduction, cut elimination and sequent calculus without cuts. The short Chapter 7 is devoted to some decidable theories, and Chapter 8 deals with constructivity.