Your question raises two interesting issues: one of formalisation, one of externalisation/reflection.  The former contains a real problem, but more philosophical than mathematical; the latter is I think where the mathematical content of your question lies, and it has a positive answer.

----------
You hit the first one on the head when you point out: "of course one could just argue that **Set1**, not being formalized, is not amenable to mathematical investigation," and I don't think your next point quite answers that question: you discuss the externalisation issues of Gödel's theorem, but that's separate from the formalisation question.  You ask for a reason to believe **Set1** doesn't prove something — how could one hope to give that without discussing **Set1** as a precise object in some meta-theory?

Fortunately, though, we don't need to posit a **Set0** for this and end up with the same problem one turtle lower down.  To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg **PA**) is more than enough.  On the other hand, we do have to presume _some_ given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory.  This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

----------
The second issue is one of reflection, and has a more satisfying resolution.  (I'll keep the meta-theory informal, but **PA** or even **HA** would be more than enough to formalise this.)  Say we have some axioms for **Set1**, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define **Set2** as the "internal version" of the same theory in **Set1**, and so on.  Now we can prove:
 
**Lemma.** (An instance of a reflection principle for provability.) If **Set1** proves "**Set2** is consistent", then it also proves "**Set2** proves '**Set3** is consistent' ".

(This is a good exercise in internalisation; it essentially comes from the fact that "being a proof" is a very straightforward property, and hence robust under internalisation.)

Now, if **Set1** is able to prove Gödel's theorem for **Set2** (in the form you state it, i.e. "if **Set2** proves consistency of **Set3**, then **Set2** is inconsistent"), we can deduce Gödel's theorem for **Set1** as follows:

Suppose **Set1** proves **Con(Set2)**.  By the above proposition, **Set1** also proves "**Set2** proves **Con(Set3)**".  Now, by G&oumldel's theorem for **Set2**, we can deduce (still in **Set1**) the theorem "**Set2** is inconsistent**".  But now we have proofs in **Set1** of both **Con(Set2)** and its negation; so **Set1** is inconsistent.  **QED**

So your question has a positive answer: if we're allowed to reason mathematically about **Set1** at all, then yes, we have reason to believe it doesn't prove the consistency of **Set2**.