In the opening chapters of Hartley Rogers, Jr.'s book Theory of Recursive Functions and Effective Computability, the proofs of the unsolvability of the halting problem and related unsolvability results invoke Church's Thesis. Can Church's Thesis be avoided?
Edit added on September 7 while putting a bounty on the question:
While in no way whatsoever doubting the diagonal argument per se, I am nevertheless in doubt as to how this is meant to work in the undecidability set up as witnessed also by my probes. One $\textit{evasion-possibility}$ that I, given my befuddlements, am not able to exclude a priori is that there $\textit{is}$ a recursive function that tells us whether a given Turing machine halts, but that a diagonalisation of the Turing machine would - pace Church and Turing - provide an effective non-recursive method beyond that recursive function.
I am rather certain that the evasion-possibility does not obtain, but I want to understand precisely why it does not. Somehow, I would have thought that the answer to this were simple. (The last sentence was not meant to contradict or undermine comments that pointed towards a tediousness of carrying these matters through.)