Logics for computer and data sciences, and artificial intelligence (Q2057567)

The book contains six appendixes: Set theory (A), Algebraic structures (B), Computability (C), Complexity (D), MV-algebras (E), Transition systems, automata, formal languages (F). I started with Appendix A. On its second and third pages alone, I spotted seven typos (\(X\) for \(x\), extra or missing parentheses). On its sixth page, the axiom of choice, that \textit{for each family of non-empty sets, \dots} is ``formalised'' as \(\forall F.F\neq\varnothing\neq\rightarrow\dots\) (nonempty family versus family of nonempty sets, hey, that sounds close enough!). Someone should at some point question why no one could be bothered. Publishers cannot be bothered with typography, they will just accept any file without performing a single edit, so \(\mathit{Tfin}(n)\) can read as \(Tf\hspace{0.3mm}i\hspace{0.3mm}n\hspace{0.3mm}(n)\) and `we infer' can read as `w e \(\mathrm{\dot{n}fer}\)'. If such comments can be made after going through just a few pages, needless to say that a very long review could be written that would do nothing but point to typos and mistakes, but let the work that has not been done by author and publisher not be work for the reviewer. To complete the review of Appendix A, suffice it to note that it contains bits on set algebra over 4 pages, on basic axiomatic set theory over 20 pages, on graphs over 2 pages including Ramsey theorem, on trees over 2 pages including König's lemma. And let us now move on to the main chapters. Chapter 1, \textit{Propositional logic}, spans 38 pages. After a first definition comes a list of 38 propositional formulas, clearly a great way to pike the reader's interest in the topic. Truth tables and normal forms are discussed, followed by axioms, rules of inference and the deduction theorem, before the proof systems of natural deduction and analytic tableaux are briefly presented, sketching a very small part of [\textit{R. M. Smullyan}, First-order logic. New York, NY: Dover Publications (1995; Zbl 1495.03002)]. Completeness of propositional logic is established, with a proof that is probably as long, contrived and unilluminating as it can possibly be. The author then jumps to Horn clauses and resolution, illustrating forward and backward chaining with a poor choice of examples and derivations, that moreover benefit from absolutely terrible typography (my mistake, I said I would not mention it any more). The last five pages quickly go over SAT solvers, logic circuits, and the perceptron. It is probably impossible to let readers gain knowledge and insights on such a diverse material in only 5 pages, even with a presentation of the highest pedagogical and formal standard, precisely the opposite of how those 5 pages can be properly qualified. Chapter 2, \textit{First-order logic}, spans 30 pages. After a confused introduction, it seems that author and publisher have united their efforts to give the most typographically appalling example of a first-order formula (so hard just to put up with it\dots). The syntax of the logic is painfully described and explained with the formation tree for the formula \(\forall x\forall y(P(x,y)\rightarrow\exists z\neg R(x,y,z))\), except that it is for the formula \(\forall x\forall y P(x,y)\rightarrow\exists z\neg R(x,y,z)\). Awesome! (My bad, I said I would just ignore mistakes.) There is then an ``introduction to semantics of predicate logic'' (aka a messy formalisation of the truth of a formula in a model), before sequents are introduced. We are told that \textit{coma in the sequent notation means disjunction}; such an interpretation on the left-hand side of sequents might indeed let readers need reanimation services if their own left-hand side cannot take this teaching. In Sections 4 and 5, the author ``returns now to Chap.1'', meaning that he takes new parts from [\textit{R. M. Smullyan}, First-order logic. New York, NY: Dover Publications (1995; Zbl 1495.03002)] to massacre it more seriously. Whereas the proof of completeness of propositional logic needed so much space and efforts, a ``form of completeness theorem for predicate logic'' comes for free, no need for the smallest element of proof; now that is nice! We get one and a half pages of valid formulas, including \(\forall x(\phi(x)\rightarrow\psi(x))\leftrightarrow(\forall x\phi(x)\rightarrow\forall x\psi(x))\). (That has to be the last time I break my promise of ignoring mistakes, however enormous they are!) We get in a swift move more proofs of completeness and of the Löwenheim-Skolem theorem, before finding out that \textit{as of yet, we have not introduced any syntactic proof mechanism}. Isn't that amazing? But that is quickly fixed, as everyone can imagine. Then comes a section on normal forms, before a section on Resolution. It would have been too much work to illustrate unification with a substitution a bit less trivial than \(x/a, z/a\), so that will do. We then discover that \textit{resolution is actually the propositional resolution whose completeness have} [sic] \textit{been proved in Chap. 1}, confirming again that in Chapter 2, we get everything for free! Section 9 offers the most impenetrable argument for the existence of a recursively enumerable, non-recursive set, thanks to which any beginner understands its ``corollary'', that the membership decision problem for type-0 grammars is undecidable. The author then seems to have remorse for such a fast treatment of the topic, and so makes it worse by \textit{giving a few necessary facts about type-0 grammars}, thanks to 10 lines, written in italics to better convey that they summarise the contents of a chapter or two of a book on formal languages. Of course the result is up to the expectations: totally incomprehensible and useless. But that's ok, that allows us to ``prove'' in no time that satisfiability for predicate logic is undecidable, before, over half a page, no more, no less, readers will be exposed to Gödel numbers, two theorems (Church and Gödel), the fact that SAT is NEXP-complete, the fact that the TQBF (whatever that means) SAT problem is PSPACE-complete, the fact that \(\Sigma_i^p\) SAT is \(\Sigma_i^p\)-complete, from which it obviously \textit{follows that any level \(o\)} (thanks for denoting it, that helps) \textit{o f t\!\!he} [sic!] \textit{polynomial hierarchy is accessible with formulae of predicate logic}. So, beginners and non-beginners united, aren't you happy to have invested in this book? Chapter 3, \textit{Propositional modal logic}, spans 26 pages. It focuses on totally standard, elementary notions and results, treated as they are in any standard textbook. In view of the kind of work that has been done in both previous chapters, that is definitely a better and safer approach. Syntax, Kripke semantics, characterisation of standard axioms in terms of the properties of accessibility relations, the five axiomatic systems K, T, S4, S5 and B are described here as they are in any introduction to modal logic. The author borrows from [\textit{M. Fitting}, Proof methods for modal and intuitionistic logics. Dordrecht-Boston-Lancaster: D. Reidel Publishing Company (1983; Zbl 0523.03013)] to extend tableaux to modal logics. General logical notions of consistency, deducibility, etc. are defined in this chapter, rather generically, without involving modal operators, as they can be indeed. It would have been better to define them earlier, all the more so in a book that goes over a number of logical systems, which would naturally suggest to unify what can be unified for a more structured and effective presentation. The techniques of filtration and bisimulation are introduced for the sake of proving decidability of all five logics. The proof of NP-completeness of satisfiability for S5 gets fuzzier, but it wisely ends the chapter. The program for Chapter 4 consists of epistemic, default and dynamic logics, with hardly more than 30 pages to, I guess, consider that the work has been done. One can wonder what justifies covering these three logical frameworks in one chapter, in this order. No justification will be provided, they will come in sequence and no attempt will be made to suggest any kind of connection. Nothing has been said so far about the non-formal part of the book. It does not mismatch with the rest, being all confused, consisting of sentences impatiently jotted down here and there. For instance, the first section of the chapter starts as follows: \textit{Epistemic logic in its present formulation is constructed on the basis of modal logics. It considers notions like knowledge and belief modelled usually by following modal logic modelling of necessity and possibility. However, one can model knowledge and belief separately which leads to strictly epistemic logics concerned with the notion of knowledge} [...] \textit{and to doxatic logics} [...] \textit{concerned with the notion of belief}. The text continues for a few paragraphs with the same kind of so insightful considerations, before the author warns the reader a couple of times that one should \textit{refer to Chapter 3 for formal introduction to syntax and semantics of modal logics}, to then \textit{notwithstanding this reservation,} [...] \textit{shortly recall the syntax of epistemic logics}. Come three pages to just replace the operator L by the operator K, and then replace (sorry, r\!\!eplace), the operator K with the operator B. We know unification of formal systems is not part of the program of the book, plus having a few pages written so easily is good to take. About time to move on to epistemic logic with n agents and learn about \textbf{EKn}, \textbf{ETn}, \textbf{ES4n}, \textbf{ES5n}, \textbf{ESD45n}, not forgetting group knowledge and common knowledge. That being done, the reader will have five pages on default logic, where of course, in the introduction, \textit{someone turns our attention to the penguin Tweety in a local ZOO} (not too sure why the zoo is local nor why it is all capitalised). About time to move on to Propositional Dynamic Logic (PDL). It will be all a succession of definitions, lemmas and theorems, except at the very beginning: \textit{PDL is a logic of action/programs based on modal logic as an archetype. We begin with regular PDF whose syntax is governed by regular expressions. Please see an account of Appendix F for an account of regular expressions}. No doubt that is more than enough to strongly motivate the reader if he or she got to this point, for seven pages of long definitions, the definition of Fisher-Ladner closure, the definition of Kozen-Parikh frames, a proof of completeness, less than half of page for decidability, validity, and complexity of PDL, to conclude with examples of validity proofs in PDL. Chapter 5 is dedicated to temporal logics. First four pages for the syntax and semantics and examples of valid formulas of Propositional Linear Temporal Logic (LTL), then three pages for the syntax and semantics of Computational Tree Logic (CTL), then one page for the syntax and semantics of Full Computational Tree Logic (CTL\(^\ast\)); another evidence that exercising pays off. Then come six pages for the ``metatheory of temporal logics'', a very technical section with results from [\textit{A. P. Sistla} and \textit{E. M. Clarke}, J. Assoc. Comput. Mach. 32, 733--749 (1985; Zbl 0632.68034); \textit{S. Demri} et al., Temporal logics in computer science. Finite-state systems. Cambridge: Cambridge University Press (2016; Zbl 1380.68003); \textit{E. A. Emerson} and \textit{C.-L. Lei}, Sci. Comput. Program. 8, 275--306 (1987; Zbl 0615.68019)], including results on model checking. Conceptual and pedagogical maturity from the original material could yield proofs that are shorter and easier to understand. Proofs are shorter, but unsurprisingly for totally different reasons. Then comes less than a page for the syntax and semantics of LTP+PAST, before a section of 1.5 pages claimed to \textit{give some insights into the vast area of model checking}. One cannot be ambitious and self-confident enough. The rest of the chapter is about tableaux for the three logics. Chapter 6 is dedicated to many-valued logics. The first and second sections are on Łukasiewicz 3-valued logic, with a sound and complete axiomatisation. The third section is the generalisation to \(n\)-valued logic for \(n>2\), with a sound and complete axiomatisation. The fourth section is on infinite-valued logics, the first half of which is dedicated to general results on t-norms. Over seven pages, the reader will read theorems referring to [\textit{C.-H. Ling}, Publ. Math. Debr. 12, 189--212 (1964; Zbl 0137.26401); \textit{P. S. Mostert} and \textit{A. L. Shields}, Ann. Math. (2) 65, 117--143 (1957; Zbl 0096.01203); \textit{W. M. Faucett}, Proc. Am. Math. Soc. 6, 741--747 (1955; Zbl 0065.25204); \textit{J. Menu} and \textit{J. Pavelka}, Commentat. Math. Univ. Carol. 17, 71--83 (1976; Zbl 0358.18007)], with no proof or a very short one accompanying those results. Considering what the author has demonstrated when dealing with elementary material, readers are unlikely to believe that what has been extracted from those papers has been adequately presented, and even more unlikely to try and disprove those legitimate doubts by attempting to study that material. The second half of the fourth section starts with the observation that \textit{a plethora of infinite-valued logics stem from various t-norms used in their constructions}, before introducing ``basic infinite-valued logic \(\mathit{BL}\)'' whose semantics and axiomatisation is briefly followed by the deduction theorem, before introducing ``the Łukasiewicz infinite-valued logic \([0,1]_L\)'' whose semantics and axiomatisation is followed by some valid inferences and formulas, before introducing ``the infinite-valued logic of Goguen'' and ``the infinite-valued logic of Gödel'' whose semantics and axiomatisations span half a page. This is followed by Section 6, dedicated to the ``complexity of satisfiability decision problem for infinite-valued logics''; over less than a page, it introduces some notation and lists three theorems. So starting with its fourth section, the chapter puts in practice again the ``accelerating presentation principle'' the reader is now familiar with. Chapter 7 is titled \textit{Approximate reasoning: rough sets}. I was really determined not to write a single word on typography any more, but sorry, this chapter brings unprofessionalism to new heights and the reader is truly entitled to feel genuinely offended for being treated with so much disrespect by the publisher. The reader who will browse (that would be remarkable already) this chapter will see the definition of an equivalence relation, basic set-theoretic operators, and the topological notions of closed and open sets, jotted down over 3 pages, just that the text also includes phrases on \textit{rough sets}, on \textit{knowledge as an ability to classify things of the real world into disjoint categories}, and on \textit{the Iris data set}. That is followed by \textit{the Rauszer functional dependence logic}, which looks so much like a standard sequent calculus that the reader would be naturally entitled to know what are the differences, and why they matter, and whether it is worth spending time on still another variant of some kind of logical system, however messy the presentation appears, however arbitrary notions and results seem to have been selected, despite of the fact that this material is unrelated to the preceding one, and to the following one, and when no true motivation has been provided here more than in any other part of the book, but of course we cannot expect that question to be addressed. Some kind of completeness result ends the section before the author can move on to \textit{the Vakerelov information logic}, telling us that \textit{these logics} (logic, logics, well, ``logical'' stuff) \textit{provide another look at information systems with the aim of directly involving attributes into logical schema}. That will do as motivation for 4 arbitrary set-theoretic conditions that can be immediately followed by a theorem with twelve items like ``\(I(u,u)\)'', then a couple of definitions and another theorem with nine items like ``\(\alpha\vee[I]\neg[I]\alpha\), then a couple of definitions and the theorem that \textit{for each filter \(F\), \([R]F\) is a filter}, then 1 page with 4 theorems with references to [\textit{D. Vakarelov}, Lect. Notes Comput. Sci. 363, 257--277 (1989; Zbl 0681.03007)]. Comes an \textit{interlude}, with the PLAY dataset (depending on outlook -- sunny, overcast or rainy -- , temperature -- hot, mild or cold -- , humidity -- high or normal -- and wind -- weak or strong --, to play tennis or not to play tennis?), here not used in the context of \textit{decision systems and rules} as advertised, but only to do the most basic kind of propositional logic, just that one can talk about \textit{information formulae}, \textit{descriptions}, a terminology that, oh misery, justifies using more than a page to ``formalise'' what \(\wedge\), \(\vee\), \(\neg\) and \(\rightarrow\) mean and state as a theorem that \(\alpha\rightarrow\beta\) is valid iff the set of models of \(\alpha\) is included in the set of models of \(\beta\). Then come close to eight pages to present and illustrate George Boole's method for \textit{finding solutions to a problem} [by] \textit{encoding the problem as a Boolean (propositional) function, converting it to a DNF and recovering solutions to the problem from prime implicants of DNF}, to be contrasted with what has been packed in half a page many times elsewhere. The chapter ends in three pages of notation and defining formulas on \textit{Nelson algebras of rough sets}, and \textit{pseudo-Boolean (Heyting) algebras of rough sets}, and \textit{the Łukasiewicz residuated lattice}. One never has a large enough collection of random definitions. In Chapter 8, \textit{Beyond first-order logics}, the author has decided to say something about first-order definability, Ehrenfeucht games, second-order logic, monadic second-order logic and connectivity of graphs, Büchi automata, Trakhtenbrot's theorem, before the final fireworks on \textit{mereological approximate logic of concepts} and 27 consequences of the three axioms of mass assignment. Each chapter ends with a set of problems, obviously without solutions or hints. I had thought that reading and reviewing this book would bring me new knowledge, offer valuable perspectives, be a fruitful and rewarding experience. May the time I wasted save the time and money of potential readers.