Theorem 4 Let C be a machine capable of processing an effective procedure P **that exists according to Theorem 1. Then, there is no formal system**
containing all computable functions that C **can generate by means of** P.

Proof. Let C **be a machine capable of processing an effective procedure** P
that exists according to Theorem 1 and let S **be any formal system with**
a predicate Q **for computable (total) functions. Because a formal system**
can be regarded as a mechanical procedure or algorithm producing provable formulas (see G¨odel 1965, p. 72), the formal system S **produces an**
effective enumeration of provable formulas Q(f1), Q(f2), ... **that contains all** computable functions f1, f2, ... in the formal system S. The machine C can generate a function g by applying the effective procedure P **to the effective** enumeration f1, f2, ... **of functions. According to Theorem 1 the function** g is a computable function that is not contained in the enumeration f1, f2, ... of functions. Therefore, there is no formal system S **containing all computable** functions that C **can generate by means of** P.

Because all programs of a programming language are finite sequences of a fixed finite number of symbols, they can be effectively enumerated, **for example, in ascending length. This implies that there is an effective enumeration**
of all computable partial functions which need not be defined for all **natural numbers. Thus, Theorem 1 implies that the function deciding whether**
or not a computable partial function is a total function is uncomputable, that is, not computable. If this function were computable, its application to an effective enumeration of all computable partial functions would yield an effective enumeration of all computable (total) functions. This contradicts Theorem 1. For these reasons, the function deciding whether a computable partial function is a total function is uncomputable. Thus, the function g in the proofs of Theorems 3 and 4, which is generated by the hypothetical machine C**, is a value of this uncomputable function that is not contained in the**
given Turing machine T and the given formal system S, respectively. Therefore, Theorems 3 and 4 imply that the hypothetical machine C **can compute**
values of this uncomputable function beyond the limits of any given Turing machine or formal system. This suggests the following definition for **a new** kind of machines.

Definition 1 A machine is called creative **if it is capable of evaluating functions, that is, determining function values beyond the limits of any given**
Turing machine or formal system.