so that both and 
are
consistent with the theory, and that of ``new axiom'', which is any
formula independent of the theory.
Mathematical Logic by Wei Li, Birkhäuser, 2010, Hard cover: ISBN-978-3-7643-9976-4
The book is entitled ``Mathematical Logic'', which will remind any logician of notorious predecessors, like [Enderton(2001)] or [Mendelson(1997)]. However, the subtitle and back cover help us to understand better the objectives of this book: to show how mathematical logic can ``provide a foundation for the development of information science and technology'' to undergraduates and graduates in information science, as well as to interested researchers. As such, the book should be compared with the existing textbooks on mathematical logic for computer scientists, like [Bradley and Manna(2007)] or [Huth and Ryan(2010)].
The book is divided into two main parts. The first five chapters present core concepts of mathematical logic; starting from there, the remaining chapters present the author own work in mathematical logic. The table of contents is briefly summed up as follows:
This part is a quite concise presentation of the core concepts of mathematical logic. The author should be praised for his survey effort. Warnings are due, however, if the readers are undergraduates or, more generally, novices in mathematical logic. The choice and presentation of the material in mathematical logic is, in fact, quite ad hoc for the second part of the book, with some exceptions. Some specific considerations follow.
Section 2 presents the classical definition of the first order formulae; no mentioning of the propositional formulae is made here. Also, no mentioning of the parsing trees is made either, whereas in modern popular books on logic for computer scientists like [Huth and Ryan(2010)], structural induction is usually explained through parsing trees. An excellent example in this respect is [Chiswell and Hodges(2007)].
Quite surprisingly for a book meant for information science students and researchers, the only proof calculus presented in the first part of the book is a Gentzen-style calculus. That said, resolution is unexpectedly introduced in the second part of the book, and limited to ``predicates with no variables'' and the ``empty sentence''...After going through all the details of the Gödel encoding, the semi-decidability of the Gentzen calculus is only informally reported in a rather compressed sentence on p. 57, and only briskly revisited on p. 116 after having presented the halting problem.
Similarly, considerations like the ``repeated'' usage of a (function) symbol is ``a characteristic of structural induction definitions'' or ``the advent of formal proofs makes it possible to convert proofs of mathematical theorems into a symbolic calculus which can be accomplished by computers within a man-machine interactive software system'' may mislead instead of helping the intuitions of novices in logic.
The work presented in Part II is motivated in the preface of the book by the following claim: ``deductive logic was well analyzed, the process of axiomatisation had not been studied in depth''. Reading it, the (logically inclined) reader can be rather unsettled at first. She needs to be patient until the opening of the second part of the book in order to grasp the meaning of the claim.
The second part opens with the author's views on the process (or method) of scientific research, which reminds the reader of Popper method (empirical falsifiability). However, no mention of it or of more recent debates in philosophy of science is being made in the opening of the second part. For the benefit of the wide audience at which the book aims, the author could better frame and ground his views and work within this area, and properly cite sources.
The first objective of the work in the second part is that of formalising the inductive process of generating new axioms and that of revising theories in the process of scientific research. The second is to ``formalize the description of research methodology and analyze the properties of sequences of theory versions''. I am not an expert in this new work and, to me, crucial notions, albeit interesting, seem in want of stronger motivations and comparison with the existing work.
The proposed framework of (version) sequences of formal theories should account for ``describing the evolution of domain knowledge''. This sounds very interesting. What the reader misses is a thorough comparison with the existing work, showing the novelty of the proposed framework. For instance, after Lemma 8.2, which states that ``default sequences'' (mentioned in Section 6.5) are special cases of version sequences, the reader is left alone to wonder what is crucially novel and relevant with respect to Reiter default logic, or other epistemic logics.
The notion of a sequence of formal theories sounds quite generic--
it can be any
countable set of theories. A similar remark applies to other crucial
notions like that of a ``new conjecture'' for a formal theory, which is
defined as any formula so that both and are
consistent with the theory, and that of ``new axiom'', which is any
formula independent of the theory.
The examples the author draws from various scientific or technological fields aim at grounding the intuitions of his new work, and as such they are potentially useful. Sometimes, however, they may mislead the reader. In the example of software development in Chapter 6, the author draws a parallel between ``the new functionality'' for a software version and a ``new axiom''. Why so and why not to, say, a new formula consistent with the theory? More generally, it is difficult to understand why the author refers to software prototyping and testing as key areas that provide new concepts to mathematical logic, without ever mentioning software verification, in which computer science and (computational) logic have already much benefited from each other, think for example of dynamic logic [Harel et al.(2000)Harel, Kozen, and Tiuryn].
The references to various branches of science reveal the wide spectrum of interests of the author, for which he should be complimented. Some quotations may still require the revision by experts in these branches, e.g., ``a photon is a rigid body'' sounds counterintuitive (a rigid body is an idealisation of a solid body, and has properties that a photon does not seem to satisfy). A minor typo: the title of the book by Galileo Galilei has ``copernico'' instead of ``copernicano''.
Given its examples and observations, the book seems to aim alternatively at a computer-science reader, novice in mathematical logic, and at times at a mathematical logician, curious about applications of mathematical logic to computer science. Some examples seem in fact to be written for the computer scientists willing to explore (mathematical) logic, e.g., ``the difference between programs and their compiled executables is precisely the same as that made between first-order languages and their models''. Elsewhere, when discussing how concepts born in mathematical logic ``like structural induction'' found their applications in computer science, the book seems to be addressing a mathematical logician.
Writing a mathematical logic book for such a varied audience is definitely a difficult job, and some readers may easily stumble upon the more technical notions outside of their expertise field. A novice in mathematical logic may feel at a loss when confronted with the digest of mathematical logic given in the first part of the book. On the other hand, the mathematical logician may find it hard to grasp the authors' motivation for the new work, presented in the second part of the book, whenever grounded in the notions or methods of software engineering.
Overall, the book seems to be more suited to a logician who is interested in the author's work, presented in the second part of the book. For others, an introductory book to mathematical logic like [Enderton(2001)] may help to complement the first part of the book.
Rosella Gennari