With the presentations by Peter B. Andrews and Lawrence C. Paulson two very different attempts to prove Gödel's Incompleteness Theorem with a high level of formalization are available, in the case of Paulson even machine-assisted. Andrews' system Q0 is an object logic, whereas the natural deduction system underlying the presentation by Paulson is a meta-logic, i. e. it is possible to express theorems of the form "a --b" or "a == b" with two or more occurences of the deduction symbol () in order to express the relationship between (the provability of) theorems rather than just theorems themselves. Paulson's proof yields a twofold result, with a positive and a negative side. It is possible to prove in the meta-logic (assuming the semantic approach and the correctness of the software) the formal statement that from the consistency of the theory under consideration follows the existence of an unprovable theorem; on the other hand, Paulson's proof demonstrates that it is impossible to prove Gödel's Incompleteness Theorem in an object logic, as it was shown for the case of Andrews' system Q0 in [Kubota, 2013], and any attempt immediately results in inconsistency. But if Gödel's Incompleteness Theorem, unlike mathematics in general, can only be expressed in a meta-logic, but not in an object logic, it cannot be considered as a (relevant) mathematical theorem anymore and is only the result of the limited expressiveness of meta-logics, in which the inconsistency of the theory under consideration cannot be expressed, although the construction of a statement like "I am not provable" has the two logical properties of a classical paradox, negativity (negation) and self-reference.