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)
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. Here
you are how I completed the chapter on the mathematical notions (Chapter 1): I
first included the basic notions that, from experience, I knew are typically
required to understand satisfactorily a text in mathematical loogc; these were so to say the bones (e.g., sets, set
relations, set operations, algebras, lattices, graphs, trees, etc). I then put
the flesh on the bones by going back to these and including in the chapter
mathematical notions that, as I was writing the main text, became necessary,
sometimes so to understand only a single
statement or exercise item (e.g., ideal, filter, hull, kernel, semigroup, etc.).
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. (Wow, four adjectives!
There is, I think, an adjective that kind of captures them all: Abstruse.) 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 qf∈Q is some accepting state qi∈A, 0≤i≤n” rather than just “if the final state is accepting”, (Yeah,
but that is hardly mathematical rigor, is it?) 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 n∈Z 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. (I’m afraid I fail to see
how.) 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)? Well, I kind of agree with Professor Martin here, but that is
the way that operators are often, though by no means always, introduced. Useless generalisation is pushed much further, resulting in endless,
contrived definitions. Surely Professor Martin realizes that they are not endless.
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). (I got –
utterly – lost here.) 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 Why
not??
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. ∀x∃yP(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.
All in all, I am rather mystified why Professor Martin did go to
the great lengths of writing such a long and detailed critical review of a book
that was completed with no pretensions other than putting together
comprehensive material, and providing a large and diverse selection of
exercises, on computational logic, namely on classical deductive computing with
classical logic. For all his apparent expertise, as an author I would have
certainly profited more from the precise indication of errors—which, given the
extension of the work and the short time I had for its completion, I knew
beforehand would be in greater number than I would be comfortable with— and
especially from the information on how to correct them. This I did by myself
when completing the 2nd edition (cf. Addenda &
Errata, 1st ed.). Perhaps Professor Martin will
now, instead of merely chastising, be so kind as to provide some useful
feedback on the 2nd edition; as an enticement, I inform him that I suspect that
not all errors in the 1st edition have been detected, let alone corrected, and
that there is likely a fresh batch of them in this 2nd edition, namely in the
new sections thereof. (P.S.: Indeed, I was right: Addenda
& Errata, 2nd ed.)
Reviewer: Éric
models of computation; classical logic; semantics; proof systems; logic programming; Prolog