Prove projection of a computable function is computable without using Church-Turing Thesis

Question

Let $R(x,y)$ be a computable relation. I want to prove that for any fixed $y$, the set $S_y$ defined by $S_y := \{ \; x\; | \; R(x,y) \; \}$ is computable. I know this can be reasoned with the Church-Turing Thesis, that is take a total TM $M$ which computes $R$ and create another TM with $y$ hardwired that then simulates $M(x,y)$. However, I was wondering if a more formal proof is possible.

Answer 1

This is fairly trivial. For a fixed $y$, we can clearly produce a Turing machine $T_1$ which, given an input of $x$, will write out $x, y$ on the tape. Because $R$ is decidable, there is a Turing machine $T_2$ which, given $x, y$ on the tape, decides whether $R(x, y)$. Then $T_2 \circ T_1$ will, given $x$, decide whether $x \in S_y$.

I do not understand how the Church-Turing thesis, which is a non-mathematical claim, is relevant here. All that is required is a straightforward application of the definition of “computable”, a term which is mathematically well-defined.