Mathematical Logic

Preface.- Glossary.- 1. Syntax of First-Order Languages.- 1.1 Symbols of first-order languages.- 1.2 Terms.- 1.3 Logical formulas.- 1.4 Free variables and substitutions.- 1.5 Gödel terms of formulas.- 1.6 Proof by structural inductions.- 2. Models of First-Order Languages.- 2.1 Domains and interpretations.- 2.2 Assignments and models.- 2.3 Meanings of terms.- 2.4 Meanings of logical connective symbols.- 2.5 Meanings of formulas.- 2.6 Satisfiability and validity.- 2.7 Valid formulas on .- 2.8 Hintikka set.- 2.9 Herbrand model.- 2.10 Herbrand model with variables.- 2.11 Substitution lemma.- 3. Formal Inference Systems.- 3.1 G inference system.- 3.2 Proof trees, inference trees, and provable sequents.- 3.3 Soundness of the G inference system.- 3.4 Compactness and consistency.- 3.5 Completeness of the G inference system.- 3.6 Some commonly used inference rules.- 3.7 Proof theory and model theory.- 4. Computability and Representability.- 4.1 Formal theories.- 4.2 Elementary arithmetic theory .- 4.3 P-procedures on N.- 4.4 Church-Turhign thesis.- 4.5 Problem of representability.- 4.6 States of P-procedures.- 4.7 System of operational calculus of P-procedure statements.- 4.8 Representation of P-procedure statements.- 4.9 Representability theorem.- 5. Gödel Theorems.- 5.1 Self-referential statements.- 5.2 Deciadable sets.- 5.3 Fixed point equation in .- 5.4 Gödel incompleteness theorem.- 5.5 Gödel consistency theorem.- 5.6 Halt problem.- 6. Sequences of Formal Theories.- 6.1 Two examples.- 6.2 Sequences of formal theories.- 6.3 Proxchemes.- 6.4 Resolution sequences.- 6.5 Sequences of default expansions.- 6.6 Forcing sequences.- 6.7 Discussions about proxchemes.- 7. Refutation by Facts and Revision Calculus.- 7.1 Necessary antecedents of formal consequences.- 7.2 New conjectures and new axioms.- 7.3 Refutation by facts and maximal contraction.- 7.4 R-calculus.- 7.5 Some examples.- 7.6 Reachability of theR-calculus.- 7.7 Soundness and completeness of the

From the reviews:"The book consists of two parts. The first part is written for undergraduate university students of computer science and presents the classical first-order predicate logic with set-theoretical interpretation of its formulas and a symmetrical, well-shaped, and beautiful Gentzen-type axiomatic system which describes identically true ... formulas of this logic. ... The second part may be used for a course for postgraduate students of information science and includes a definition of versions of a formal theory, version sequences and their limits." (Alex Nabebin, Zentralblatt MATH, Vol. 1185, 2010)