What Gödel Discovered

Your procedure of repeated substitution in order to resolve a paradox does little to shed light on the situation since at the heart of the halting problem is that there's no formal system that can determine whether this repeated substitution will ever come to an end.

Sure in your trivial example we could prove that it never comes to an end and determine that the statement is a paradox and label it as such, but there are some statements where it's not clear whether there's a paradox in the first place and there are some statements that are a paradox in one interpretation but in another interpretation are perfectly sensible.

Rest assured, no mathematician is scratching their head wondering whether "This statement is false." is some kind of mysterious statement whose undecidability has profound consequences. The issue is with statements like whether there exist 3 integers, x, y, z such that:

x^3 + y^3 + z^3 = 114

That statement in and of itself may very well be a "paradox" similar to a statement such as "This statement has no proof in theory T." even though on the surface it looks like a perfectly reasonable equation that should either have a solution or not have a solution. I mean either three such numbers exist or they don't exist, right?

And yet... it's possible that for the equation I gave there are solutions only under some interpretations of what we normally call natural numbers and in other interpretations of what we call natural numbers there isn't a solution, and there's no formal system that can filter out one interpretation over another so that there is one and only one unambiguous interpretation of natural numbers that we can always rely upon as the "real" interpretation.

There are perfectly normal looking sentences and problems that on the surface don't appear at all to be paradoxes or self referential, but then become so when you try to pin the question more precisely.

That's where the fascination comes from, from looking at a seemingly normal looking equation or statement about numbers that should just be true or false and realizing that whether it's true or false depends on some very deep and as-of-yet unknown properties of what we even mean when we talk about natural numbers.

Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification.

Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.

The Godel sentences are of a different character than the continuum hypothesis (CH) because the Godel sentences are simple first-order arithmetic statements, while the CH is a higher-order, a.k.a. analytic statement. A Godel sentence can be assigned a truth meaning via Tarski's definition of truth independent of the axiom system in a way that is much harder to do with the CH.

Basically a Godel sentence says something about whether a given piece of software terminates when run on an ideal computer (specifically a piece of software that hunts for a proof of a contradiction within a specified axiom system). I'll argue that whether a specific piece of software would halt or not when run on an ideal machine has a definite truth value independent of any axiom system. Whereas CH doesn't really afford such a software interpretation.

I do respect the fact that there exist models of PA + ~Con(PA) but these models are non-standard and we don't use such models to reason about software, specifically because they are unsound in this sense.