If you are referring to page 259-262 of Turing's paper, the proof that formula CFn is provable, for every n, is by induction.
It is a meta-theory proof, because it is about formulas and their derivability ("provability") in the formal system.
The proof is standard proof by Induction:
(i) Base case: CF0 is provable.
(ii) Induction step: formula CFn → CFn+1 is provable, for every n.
Thus, by Induction, we conclude that CFn is provable, for every n.
Now, the issue is: what is the exact meaning of "formula CFn is provable" ?
It is derivable in predicate calculus.
See page 259:
[...] to show that the Hilbert Entscheidungsproblem (the problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid) can have no solution.
I propose, therefore, to show that there can be no general process for determining whether a given formula A of the functional calculus K [see David Hilbert's and Wilhelm Ackermann's Grundzüge der theoretischen Logik (1928), Ch.3] is provable, i.e. that there can be no machine which, supplied with any one A of these formulae, will eventually say whether A is provable.
Corresponding to each computing machine M we construct a formula Un(M) and we show that, if there is a general method for determining whether Un(M) is provable, then there is a general method for determining whether M ever prints 0.
Thus, trying to be more "formal", the result you are referring to amounts to (see "turnstile" symbol):
⊢K CFn, for every n,
where ⊢K CFn means:
"there is a derivation of formula CFn in functional calculus K."
Additional note: as said above, the induction is performed in the meta-theory, because it applies to formulas.
We have an infinite sequence of formulas: { CF0, CF1, ..., CFn, ...} and we consider the property P(n) := "formula CFn is provable (in functional calculus K)".
We prove that CF0 is provable, i.e. that P(0) holds, and we prove that: "if CFn is provable, then also CFn+1 is provable, for n whatever".
Thus, applying Mathematical Induction, we conclude that P(n) holds for every n, i.e. that:
"CFn is provable, for every n.
Turing writes "CFn → CFn+1 is provable" instead of "if CFn is provable, then also CFn+1 is provable".
There is no difference; in symbols, from ⊢K CFn and ⊢K CFn → CFn+1, by Modus ponens we have ⊢K CFn+1.