The following* is a negative review by Professor Eric Martin of the first edition of this textbook. I see my books (and papers, too, for that matter) as work in progress, and thus am thankful for all feedback that might help me in this task. This I do, at a time when the Internet allows for a (Marxist) real-time flow of information, by posting online and regularly updating addenda and errata lists, and by eventually completing new editions with the additions and corrections as soon as it is feasible. While I thank Professor Eric Martin for his scrutiny, which I was not timely aware of for the completion of the second edition (published in January, 2020), I cannot but disagree with some of his criticism. In due time, I hope to be able to reply to all his concerns by commenting on his original text with this font in this color.

 

* https://zbmath.org/?q=an%3A1408.68001 (Retrieved on Feb. 10th, 2020)

 

 

 

Augusto, Luis M.

Computational logic. Volume 1: Classical deductive computing with classical logic. (English) Zbl 1408.68001

Texts in Computing 19. London: College Publications (ISBN 978-1-84890-280-0/pbk). xviii, 464 p. (2018).

Following an 11-page introduction, the book is divided into four parts. Apparently, there is nothing wrong with the introduction, though running at 11 pages, as it does, a lot of things could have gone wrong. {

\begin{itemize}
\item[–]Mathematical notions: Set-theoretic concepts. Boolean algebras. Lattices. Graphs and trees. Mathematical induction. 
\item[–]Classical computing: Formal languages and grammars. Regular languages. Context-free languages. The pumping lemmas. Derivations and ambiguity. Recursively enumerable and recursive languages. The Chomsky hierarchy. Deterministic and indeterministic finite-state machines. Decision problems. Transducers, Moore and Mealy machines. Deterministic and indeterministic pushdown automata and acceptance criteria. \(LR(0)\) and \(LR(1)\) grammars. Deterministic and indeterministic Turing machines. Linear bounded automata. Turing-reducibility. The Halting problem. Space and time complexity classes. Polynomial-time reducibility, NP-completeness and NP-hardness. 
\item[–]Classical deduction and classical logic: Propositional and first-order languages. Inference rules. Valuations and interpretations. Logical consequences, satisfiability. Completeness. Undecidability, decidability and complexity of first-order classes of languages. Substitution, unification. Equality. The Frege-Łukasiewicz axiom system. Natural deduction. The sequent calculus. Tarskian semantics. Herbrand semantics. Algebraic semantics. 
\item[–]Classical deductive computing with classical logic: Proof of NP-completeness of the satisfiability problem. Normal forms (prenex, Skolem, NNF, CNF, DNF and special cases of the satisfiability problem. Herbrand’s theorem. Resolution for propositional logic and first-order logic. Hyperresolution. The Prover9-Mace4 theorem prover software. Paramodulation (equality in resolution). Analytic tableaux for propositional logic and first-order logic. Logic programs. SLD-resolution. Prolog. Negation as failure. 
\end{itemize}

} So the monograph provides introductory material to three fields of study: automata theory, logic, and logic programming. Since there is a plethora of publications for all three, most readers will likely have at least two expectations: that the structure of the book ties those fields of study as closely as possible; and that what is standard, classic material be presented in a way that benefits from decades of experience and be of high pedagogical value. Unfortunately, readers will most probably, very quickly find out that the book fails on both accounts, that the formal presentation is of very low quality, and they might even become extremely frustrated and conclude that for any part of the material, there are many sources of information where a much better job has been done. Readers’ expectations should be objectively based, i.e. based on information provided in the book, namely on the back-cover synopsis. This, in the case of this book, reads as follows: “The objective of the main text is to provide the reader with a thorough elaboration on both classical computing and classical deduction with the classical first-order predicate calculus with a view to computational implementations. As a complement to the mathematical-based exposition of the topics we offer the reader a very large selection of exercises. This selection aims at not only practice of discussed material, but also creative approaches to problems, for both discussed and novel contents, as well as at research into further relevant topics.” Nowhere in this passage – nor elsewhere in the book, for that matter – is it claimed “that the structure of the book ties those fields of study as closely as possible” and/or “that what is standard, classic material [is] presented in a way that benefits from decades of experience and [is] of high pedagogical value.”

There are many merciless enumerations of definitions in sections that too often are not well-structured. For instance, we have Definition 1.2.1 on algebraic structures, then Definition 1.2.2 on abstract algebras and related concepts, further extended to 13 more concepts in Definition 1.2.3, then Definition 1.2.4 that briefly talks about semigroups, partially-ordered semigroups and monoids, and then Definition 1.2.5 which starts with the sentence “let B=(B,′,,,0,1) be a Boolean algebra”, whereas the notion of a Boolean algebra has not been previously defined, plus that alleged definition actually reads as a list of properties. Definition 1.2.1 is meant to provide the important information that the triple (A, O, R), where A is a non-empty set, O is a set of operations on A, and R is a set of relations on A, called an algebraic structure (or system), may contain two distinct yet often related structures, to wit, an algebra – (A, O, ) – and a model – (A, , R). Both structures are central in classical first-order predicate logic and are accordingly ubiquitous in this book, with the difference that the former is more used at the metalogical, namely foundational, level while the latter is a metalanguage notion simpliciter that is very frequently used in the main text.  (Please note that though metalogic and metalanguage are related concepts, they are not (absolute) synonyms.) Mostly for this reason, the emphasis in this Chapter 1 (entitled “Mathematical notions”) is on algebras; this emphasis is reflected on a definition giving the basic features of an algebra (Def. 1.2.2) followed by another definition (Def. 1.2.3)  comprising 8 distinct notions that are relevant for the main text, to wit, subalgebras, reducts, similar algebras, morphisms (homomorphism, monomorphism, epimorphism, isomorphism), the least sub-algebra, generators, absolutely free algebras, and C-free algebras (where C is a class of similar algebras). All these having been defined, we can define a specific algebraic structure (X, *) where * is a binary associative operation on X, which becomes a monoid with the addition of the distinguished element 1 (in this case). (Note that the reader has already been given the definition for n-ary operation on some set A (cf. Def. 1.1.6). To be sure, associativity has not been presented, but one can expect that anyone who has been properly schooled must somehow be able to recall this property. And other basic concepts, for that matter, as otherwise one takes the reader as a tabula rasa in the Lockean sense.) This definition is brief, because it will be recalled only in Def.s 2.1.7-8, and very briefly so, given that, as is usually the case, one does not elaborate on the topic in an introductory text. Finally, “Let X be so-and-so” is, indifferently, a way either to introduce a new concept or to retake some already given one. In this particular case, the reader knows from Def.s 1.2.1-2 that the pair (A, O) for some non-empty set A and a set O of operations oi, 0 < i n, is an algebra; as a matter of fact, the  reader already has been given examples of algebras (cf. Example 1.2.1 and Def. 1.2.4). Hopefully, it will not be (too) difficult for the reader to realize that (B, ΄, ,, 0, 1) is another algebra, namely an algebra of type 5 (cf. Def. 1.2.2), which, as it is, is a Boolean algebra iff it has the properties, or satisfies the conditions, that follow. To be sure, I could have formulated this as “Let B = (B, ΄, ,, 0, 1), where B is a non-empty set, etc. etc. be an algebra. Then, B is a Boolean algebra if …”, but then I might be chastised for engaging in unnecessarily over-detailed formulations, as below I am.

Besides the lack of structure and the slackness of presentation, the reader can legitimately wonder whether all those notions will eventually be used, and for those that will (as indeed not of all them will), where in the book that is, and whether this or that notion is promised to play an essential or a marginal role. The fact that the Index is minimal (e.g., “semigroup”, “monoid”, and even “algebra” are not part of the Index) seems to imply that readers have no other option but memorise them all, in their driest form, in case they turn out to eventually prove useful, as indeed the author does not always refer to where a notion is defined in case it is eventually used; when he does refer to a definition, it is often a nightmare to spot it, as definitions, theorems, examples, etc. are numbered independently and interfere. Professor Martin thinks the Index is minimal; I think it is proportionate. In particular, the mathematical notions of Chapter 1 are essentially omitted in the Index, as I guess the reader will autonomously self-refer to it in case of need. I also expect that anyone who can count to, say, 100, will be able to navigate easily in the numbered items in this book, even if, as sometimes is the case in other published texts, theorems and examples are numbered independently. But then, by posing an intellectual challenge of such a proportion as Professor Martin claims the numbering in this book does, I might have unwittingly given this book also the convenient property of staving off early onset dementia. The one more reason for you to peruse it.

 

Definitions are often imprecise, awkward, fuzzy, unclear. For instance, Definition 2.2.4 differentiates between a string that is “accepted” and a string that is “recognised”. Most readers would be hard pressed to understand the difference between both notions from the proposed definitions, and will be irritated at phrases of the form “if the final state qfQ is some accepting state qiA, 0≤in” rather than just “if the final state is accepting”, all the more so that a prior definition introduced the notation with a set A of accepting states, not a state of cardinality n+1 for some integer n that is in fact introduced earlier in Definition 2.2.4 to denote something totally different (the last index of a sequence of configurations). Even worse, the text is full of more or less serious mistakes. For instance, in Example 2.3.1, meant to demonstrate that the set of polynomials over x with an integral root is not decidable, we read “if some nZ it is the case that p=0”, which is formally very slack, to say the least, before having to remark that it is “obvious” that the specific algorithm that consists in, for a given polynomial p, enumerating values x and testing whether p(x)=0

, “will run forever”, and then conclude: “thus this set is in fact not computable”, thus being both grammatically and logically wrong\dots. These are just examples, randomly chosen as almost each and every page of the book could be used as an illustration of the poorness of presentation.

Generality is good, only if it proves useful, only if it is not gratuitous. For instance, what is the point in Definition 3.1.3 of writing “if ni

is an n-place operator and ϕ1, \dots, ϕn formulae, then i(ϕ1,…,ϕn) is a (compound) formula” when operators will then be nothing but negation and the usual binary Boolean operators (not to mention the useless introduction of the index i)? Useless generalisation is pushed much further, resulting in endless, contrived definitions. For instance, after the long Chapter 3 on logical form and logical meaning, where way too many definitions were introduced to awkwardly present the basic syntax and semantics of logical systems, Chapter 4 re-attacks with for instance Definition 4.2.1 to introduce “Tarski-style conditions for the classical consequence operation CnL for a (possibly empty) set ΓFL and any formula ϕ,ψFL”, such as “Cn(Γ,ϕψ)=Cn(Γ,ϕ,ψ)”, whereas in Chapter 3, means conjunction, but the fact that “classical” occurs in the title of Chapter 4 probably prompted the author to specialise what would be a potentially more general interpretation where would not mean conjunction (with as usual, messy notation, here, in particular and not exclusively, with the introduction of L as a subscript to Cn that is then immediately dropped). The lack of coherent structure strikes everywhere. For instance, after the long Chapters 3, 4 and 5 all dedicated to the syntax, semantics, and proof theory of propositional and first-order logic, the more specialised Chapter 6 on “Algebraic semantics: Boolean algebras” ends with two absolutely basic syntactic definitions: “An expression of the form ϕ(p1,…,pn) where the pi are propositional Boolean variables is called a propositional Boolean formula” and “An expression of the form 1x1…nxn(ϕ(x1,…,xn)) where the xi are individual Boolean variables and the i{,}

is called a quantified Boolean formula” (with expectedly, unnecessarily unfamiliar symbols, unnecessary indexes, unnecessary parentheses\dots); why here? why there at all?\dots

The book is full of exercises, of four kinds. First, straightforward exercises to test the understanding of basic notions, for instance, Exercise 3.1.2.3: “Identify the closed and the open FO formulae. For the open formulae, give their universal closure. 1. xyP(x,y)

\dots”. Second, exercises where the reader is asked to complete the proof of a result in the text, for instance Exercise 3.5.3.4: “Complete the proof of Theorem 3.5.8”. Third, exercises which are just classical results that the text left out, for instance Exercise 3.5.1.2: “Let Θ be an axiomatizable theory. Show that if Θ is complete then Θ

is decidable.” Fourth, very open-ended exercises, for instance Exercise 2.3.12: “Research into Post’s Correspondence Problem and give its main points”. While it is good to have many exercises, those proposed in the book do not have much originality and not much thought has been given to making sure they are as insightful and valuable as possible. As an instructor, when using a textbook I like to have a large selection of exercises from which to choose those that might better fit the students’ skills and capabilities. The range of these is pretty (impressively) wide, and at this introductory level, at which the main objective is that students grasp the basic concepts by both practicing and ruminating, I am not really concerned with originality; as an author, thought is given to making sure that the exercises might contribute to this objective.  Most results are given in the text without proof (that is, are given with a proof that refers to an exercise asking for the proof), while most remaining results are given incomplete proofs, with again one reference or more to exercises asking to complete this or that part of the proof. Many readers would probably prefer to have a more self-contained body, with carefully written, complete proofs that prepare them better to tackling exercises, but it is true that considering how poorly proofs or proof sketches are written, the current design might still be preferable\dots A more self-contained book is hardly possible, as the second edition already runs at over 330 pages and there are still contents I think should be covered (e.g., formal verification). Giving complete proofs of all the main statements, while significantly taking space from more important contents would not bring any benefits for, in my view, mostly two reasons: firstly, complete proofs, original or in a different guise, are to be found in just about any “standard” book in the field and no book, self-contained or not, stands alone; secondly, my objective is that students learn how to make their own proofs. With the latter aspect in mind, when giving a complete proof I try to be as concise as possible, and when giving a sketch of (or just an idea for) the proof I aim at omitting some aspects that would perhaps make the proof-writing too easy an exercise. To be sure, this might conduce to what can be seen as “poor writing,” especially if one’s pedagogical objectives are stifled by one’s authorial aspirations.    

There is substantial general, “philosophical” discussion that is consistently confused, unclear, meandering, and not illuminating at all. This sounds pretty much like most “philosophical” discussions. In any case, maybe I should be flattered, given that, despite my training (also) in philosophy, I did not intentionally engage in any “philosophical” discussion in this book.  The claim that with logical languages we are “not interested in formalizing questions, orders, commands, interjections, or ejaculations” seems to be the only spurt of humour. It is my turn to be puzzled: This was a spurt of humor? Was humor expected in a book entitled “Computational logic”?

The typography is terrible. Arguably, the author should not be the only one to blame: this criticism would be alleviated or would disappear if publishers did not consider that their job does not go beyond accepting any Latex file without bothering to quickly browse how the pdf looks like and perform minimal edits. I really don’t know what the curt statement “The typography is terrible” is meant to convey, as no specification is given, but one of the many reasons that made me decide to publish with College Publications, London – to the extent that they accept my submissions, that is – is the low cost of the books, a feature that aims at making information accessible to all. Professional proofreaders and typesetters would significantly increase the prices of the books. This said, I can assure critics that no potential issue passes undetected before a book is eventually published by them.

A second volume on nonclassical logics is promised, but it would not be surprising that most readers who have tried to study the first volume will not consider learning from the second one.

Reviewer: Éric

 

 Martin (Sydney)

MSC:

68-01

Introductory exposition (textbooks, tutorial papers, etc.) from computer science

03B70

Logic in computer science

68N17

Logic programming

68Q05

Models of computation (Turing machines, etc.) (MSC2010)

68Q15

Complexity classes (hierarchies, relations among complexity classes, etc.)

68Q17

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

68Q42

Grammars and rewriting systems

68Q45

Formal languages and automata

68T15

Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

models of computation; classical logic; semantics; proof systems; logic programming; Prolog