In Turing's article 1936 https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf Turing provides a proof in §11 p.259 for the Hilbert decision problem "Entscheidungsproblem".
p. 259 he says "I propose, therefore, to show that there can be no general process for determining whether a given formula U of the functional calculus K is provable"
For that, he constructs for each Turing machine M a formula Un(M) p. 260, and proves in Lemmas 1 and 2 that
"M ends up printing the 0 symbol" iff Un(M) is provable.
I understand the notion of Hilbert formal proof of a formula F in a theory T, in standard notation T |- F .
I do not understand which signature L he is using for constructing Un(M) as a first order formula ?
And when he says "provable", which theory T in this langage L is he refering to ?
What is to be meant by "Hilbert functional calculus K" in relation with modern presentations of proof theory in the context of first order theories ?