Mendelson concedes that a significant part of my case succeeds, that is, that (4) is indeed false: He agrees that the formal concepts in question (e.g., `Turing-computable function') are more useful than their informal partners (e.g., `effectively computable function'); and he admits that ``One could, with some justification, claim that the notion of a Turing-computable function is `clearer' than that of an effectively computable function because the former is more specific and ties in closely with other well-known mathematical concepts." However, Mendelson goes on to say:
My point in this case has nothing to do with relative clarity of concepts. Rather, the point is that the notion of an effectively computable function is not essentially different from the notions that underlie the theory of Turing-computable functions, and, more specifically, that the former notion can be used in mathematical proofs just as legitimately as the latter notions. This was illustrated in my paper by the proof that all partial-recursive functions are effectively computable. That proof, which Professor Bringsjord himself accepts, undermines the basis for the traditional belief in the unprovability of the the Church-Turing Thesis, namely, that there is in principle an unbridgable gap between, on the one hand, arguments that involve `vague, intuitive' notions, and, on the other hand, `respectable' proofs that can be formalized within, say, ZF or PA.
Unfortunately, this rebuttal fails. Yes, I did indeed concede that Mendelson's mathematical argument for the so-called ``easier" half of CT constitutes a proof (though I think Mendelson's comment following that argument -- ``This simple argument is as clear a proof as I have seen in mathematics" (233) -- is at least peculiar, and possibly disingenuous). But Mendelson seems to ignore my observation that his proof doesn't substantiate the premise in Arg1 called `EQU:'
Lest it be thought that I tendentiously cooked up this premise, and set it as an unreachable target for Mendelson, I remind the reader that the text in question is clear: there can be little doubt that Mendelson targets EQU. Consider again, for example, what he says on page 232:
Here is the main conclusion I wish to draw: it is completely unwarranted to say that CT is unprovable just because it states an equivalence between a vague, imprecise notion (effectively computable function) and a precise mathematical notion (partial-recursive function). ([27], p. 232; emphasis mine)
And again on page 233 Mendelson says that ``equivalences between intuitive and `precise' notions need not always be considered unprovable theses" (emphasis mine).
Now Janet Folina [15] has suggested that Mendelson's aim be charitably scaled back -- so that what he is said to be aiming at is not a demonstration that CT is provable (an aim she agrees I have shown Mendelson cannot reach), but rather a demonstration that proofs merely connecting intuitive with formal notions are possible. This reconstruction of Mendelson's main argument is, predictably, one that I would gladly accept.12
With our foundation laid, I turn now to my narrational attack on CT.