It's an example - but one that doesn't relate to the problem at hand, which concerns whether a machine returns 1 - or not. If you ASSUME some particular axiom and proof system, the problem becomes easier. However, with no specified axiom system for generating proofs - and no specified proof checker - then the problem becomes poorly-specified.

Regarding Tarski's theorem - you seem to be misinterpreting me. I am not saying that checking a proof with respect to an axiom system is necessarily difficult. I am saying that truth is not contained by any finite axiom system. So, there will be true statements that are unprovable within the system - but can still be proven in a larger system. That is also what Tarski's theorem happens to say. Check it out:

"The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in N is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC."

• http://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem