Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The foundations of computability theory
Robic B., Springer Publishing Company, Incorporated, New York, NY, 2015. 331 pp. Type: Book (978-3-662448-07-6)
Date Reviewed: Apr 19 2016

This book serves as an introduction to computability for readers who are somewhat familiar with mathematics and logic. The brief appendix of notions and notations is useful, but does not provide standalone orientation. For the prepared, this is a wonderful blending of history and philosophy, foundations and computation, math and the mystery of the incomplete, undecidable, unknowable, incomputable. Nonetheless, this is a wholly introductory book, and a willing reader will be happy.

The first four chapters start with a preliminary discussion of algorithms, and then present a standard and sympathetic view of logicism, intuitionism, and formalism. Next, the trio is invoked in decoding the eruption of computation models in the early 1930s. Making a wise choice to focus on Turing machines (wise if only because they are computer-like--but for other good reasons as well), the development proceeds to unite the different models and set the terminology (using Soare modern). After incompleteness, universal Turing machines, and incomputability, topics advance to Rice’s theorem, priority methods, and the arithmetical hierarchy.

Throughout there are sidebars giving the fine print of more technical details, indeed in finer print. These are still accessibly informal.

The author offers this book as a gateway to more serious, more formal computability books and surveys. Such an entrance should be celebrated, and when the following sorts of difficulties are overcome, I will heartily endorse this one.

First, some good points. Following Rogers [1], the Church-Turing thesis (CTT) is used as a heuristic for formalizing the existence of algorithms that have convincing descriptions if not definitions. On page 58, a fine remark points out that other methods may prove sentences that appear true but cannot be settled from a first-order axiom system. (An example could be Kalmár’s proof of Gentzen’s theorem on the consistency of PA, using a single invocation of Carnap’s rule with induction to &egr;0, a minimal extension.) On page 71, it is recognized that to approach the defeat of the Hilbert program (even as a negative solution to H10) requires a useful, careful, formal notion of algorithm.

There are several sorts of shortcomings. Some are trivial--typographical errors, bad turns of grammar, or minor math missteps. For example, notation is sometimes used before it is introduced (as with quantifiers and connectives on page 22); here, the notation lists and appendix help. As another example, ψ is supposed to be ψe at the top of page 153. Also, in Box 9.1 on page 207, it should be ψx ≠ ψf(x), instead of xf(x).

Some other shortcomings are more serious and should have been caught by mathematical copy editing. For example, in Box 3.2 on page 40, the ∀-instantiation scheme (L4) includes “if t can be substituted for x,” but it does not specify substitution and the range of t is a big guess. Equality axioms are not given, but at least they can be deduced in arithmetic A on page 41. L axioms are said to include P axioms (or some of them), but P axioms/rules are not defined in the book. Either A2 ∀xy(x=yx’=y’) is pointless (in light of equality and substitution), or one can (and must) use it with induction to prove the required versions for +, ×. On page 44, it is not clear whether ZF axioms cover equality. Better if ZFC1 is ↔. Also, the Padding lemma on page 146 is just misstated; “the others” means “the others described in the proof” or “countably infinitely many others.” Theorem 8.1 on page 166 is incorrectly stated. DSub must be a decidable subset of DProb. The cases discussed in 8.2 on that page should use “semi-decidable (and not decidable).” As another example, the list of undecidable problems on page 173 contains: “Does M halt on w?” where M is a fixed TM, and w is a varying input word. Of course, this depends on the choice of M. For some M, M halts never, for some M, M halts always, and so on. It should be: “Does T halt on w0?” Here, T varies, and w0 is fixed. Note the correct version at the top of page 176.

Finally, some shortcomings read as if an alternate universe had been entered. First, there is a confusion in the “semantic completeness” discussion on page 52. By the completeness theorem, every theory is semantically complete. What is intended here is the “intended” semantics. This is explicitly revealed on page 57, where it says there are sentences true of the natural numbers that are not provable in the theory A. But any sentence true in all models of A is provable from A, by the very method he describes, namely using the completeness of L and taking implications with axioms as premises (even when there are infinitely many axioms, and they are not a computable or c.e. set).

In another example, on page 92 , a diagonal argument concludes that a constructed total function g is not computable, although it appears to be. The claim is boldly repeated on pages 191-195 (especially Example 9.2). For some reason, the real falsehood is not produced: there is no computable enumeration of the total computable functions. Despite the full discussion and acceptance of CTT as the formalization of computable functions, the text twice claims that g is computable but not recursive (the word has its uses). For a “real” proposal of such a function, consult [2].

Tarski should be given credit for inventing decidable theories, and his decision procedure for real-closed fields deserves citation. Many other results among topics in the book could be listed, primarily the definition of truth and the notion of metalanguage. But to attribute conversion to prenex normal form (PNF) to Kuratowski and him on page 284 seems to be an overreading of Rogers [1, chapter 14.3], who does not claim PNF for the Tarski-Kuratowski algorithm. Nor do Tarski and Kuratowski [3,4]. Peirce discussed prenex form in 1885 and presaged PNF [5, pages 196-198] if not demonstrating it at full strength.

Reviewer:  Benjamin Wells Review #: CR144334 (1607-0466)
1) Rogers, H., Jr. Theory of recursive functions and effective computability. McGraw-Hill, New York, NY, 1967.
2) Pkhakadze, Sh. S. An example of an intuitively computable, everywhere defined function and Church’s thesis. Tbilisi State University, Georgia, USSR (Russian, with English summary), 1984.
3) Kuratowski, C.; Tarski, A. Les opérations logiques et les ensembles projectifs. Fundamenta Mathematicae 17, (1931), 240–248.
4) Kuratowski, C. Evaluation de la classe borélienne ou projective d’un ensemble de points à l’aide des symboles logiques. Fundamenta Mathematicae 17, (1931), 249–272.
5) Peirce, C. S. On the algebra of logic: a contribution to the philosophy of notation. American Journal of Mathematics 7, 2(1885), 180–196.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Computability Theory (F.1.1 ... )
 
 
Modes Of Computation (F.1.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Computability Theory": Date
Decidability of the purely existential fragment of the theory of term algebras
Venkataraman K. Journal of the ACM 34(2): 492-510, 1987. Type: Article
Jul 1 1988
Computability
Weihrauch K. (ed), Springer-Verlag New York, Inc., New York, NY, 1987. Type: Book (9789780387137216)
Nov 1 1988
Computability and logic: 3rd ed.
Boolos G., Jeffrey R., Cambridge University Press, New York, NY, 1989. Type: Book (9789780521380263)
Jul 1 1990
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy