Does proof of FOL undecidability require tacit appeal to the Church-Turing Thesis?

Question

We can prove that FOL is undecidable using a strategy based on the undecidability of Q. But does this latter proof require tacit appeal to the Church-Turing Thesis?

Answer 1

No, it does not. However, if you're not careful about interpreting the statement

$(*)\quad$ $\mathsf{Q}$ is undecidable,

it may seem necessary.

See also my answer to essentially the same question on philosophy.stackexchange.

---

"Undecidability" is a technical term referring to the specific formal notion of computation given by Turing machines, and $(*)$ above is a genuine formal theorem to which the Church-Turing thesis is totally irrelevant. This will become clear if you read the proof in detail.

• Note btw that Godel's incompleteness theorem predated the introduction of Turing machines, and hence Godel's acceptance of the Church-Turing thesis, by five years. Of course Godel wasn't talking about $\mathsf{Q}$, but Robinson introduced $\mathsf{Q}$ as a finitely axiomatizable theory for which Godel(/Rosser)'s argument goes through without serious change. So we can see right off the bat that Church-Turing can't possibly be relevant here.

---

On the other hand, we also have the statement

$(**)\quad$ There is no algorithm for determining whether a sentence is a theorem of $\mathsf{Q}$. Or put another way, the problem of telling whether a sentence is a theorem of $\mathsf{Q}$ is not effectively solvable.

Now there's a crucial issue here, in that $(**)$ is an informal statement: "algorithm" and "effective solvability" are informal terms, referring to some imagined ideal notion of human computation. One consequence of the Church-Turing thesis is that $(*)\iff (**)$, and so the formal (and thesis-free) proof of $(*)$ tells us that $(**)$ is true. But this is the only place where the thesis comes in: it's not relevant to the proof of $(*)$, only to the claim that $(*)$ and $(**)$ "mean the same thing."