Cantor's diagonalization argument shows that uncountable sets exist, and they are different from countable sets. That was sufficiently counterintuitive that so

Cantor's diagonalization argument shows that uncountable sets exist, and they are different from countable sets. That was sufficiently counterintuitive that some mathematicians rejected it at first, until they warmed to the idea. Your circular dependencies are metacircular rather than circular. That corresponds to circular if you can prove that truths in the system and its metasystem are equivalent, but that's often not so easy to show rigourously. (In other words, so you can be really really sure you haven't missed a subtle loophole). It's tempting to assume they are equivalent by intuition, but that assumption isn't correct for all logic systems. Like many good theorems, the core idea is simple once explained. Gõdel's incompleteness theorem required the axioms and logical deduction rules of the arithmetical logic used at the time to be encoded using that very same arithmetic, and to prove that's possible, that it works, and it's consistent. That takes some rigour. Until it was done, it wasn't obvious you could definitely prove that it works, because system-metasystem relationships often have some subtle twist. My favourite example of a subtle twist like that is Skolem's Paradox. Which relates back to diagonalization, and shows that maybe countability and uncountability aren't so simple after all.