On (1). In more standard terminology:
A formal theory is [negation] complete if for each sentence (closed formula) φ either φ or ¬φ is provable.
A logical deductive system is semantically complete if every sentence (closed formula) φ of the system which is a logical truth is provable.
Gödel's incompleteness theorem shows that first-order Peano Arithmetic isn't negation complete. (And trivially, since one of either φ or ¬φ is true on the standard interpretation, there is a truth PA can't prove).
But the first-order deductive system built into PA is still semantically complete (by Gödel's completeness theorem!).
It was/is important that Gödel's official incompleteness result is a purely syntactic one, proved on purely syntactic assumptions. For recall the context back around 1930. Semantic notions (pre-Tarski) were widely thought murky and "unscientific"; and the major research programme in foundations in Gödel's environment was the Hilbertian program which presupposes that we can completely axiomatize swathes of mathematics. Showing on syntactic assumptions that the Hilbertians would have to buy that we can't even get a complete theory of elementary arithmetic was therefore devastating.
Your question makes sense to me, but it's a bit hard to answer concisely. The short answer is that for the most part, when mathematicians decide to accept anything as true, it is because it has been proven rigorously. And as you allude to, rigorous reasoning lends itself to an analysis where we convert the reasoning into a formal proof in some system (say PA, or ZFC). When you come up with a semantic proof for the truth of something by considering models (or truth tables for propositional logic), you are using reasoning that can be formalized in ZFC or in rare cases, some somewhat stronger system. In fact 'mathematically accepted fact' roughly correlates with 'has a proof formalizable in ZFC.' Thus, formal proofs are always there... it's really the only way we know to clearly establish mathematical truth.
Some of your thinking seems to stem from overgeneralizing from the example of propositional logic. Frankly, I'm a bit surprised your instinct was that formal proofs are the more convenient method here. A formal proof can be tedious to find, even in the case of propositional logic, especially if you're using an inconvenient Hilbert-style system. On the other hand, what could be easier than just plugging in some values to a truth table? (conceptually... computationally, the problem does not scale well).
However, this is an artifact of the fact that propositional logic is decidable. If we move on to first order logic, we're faced with difficulty: how do we decide if every $m\in M$ satisfies $\phi(m)$ for $M$ some structure and $\phi$ some formula of its language? We no longer necessarily have a decidible problem. The "brute force solution" would be checking $\phi(m)$ for every $m\in M,$ which cannot be done if $M$ is infinite (and who knows if $\phi(m)$ is decidible itself). It turns out that this basic difficulty is not surmountable in general, and Godel's theorem and the halting problem are ways of seeing this.
To show that a sentence is true in the structure $\mathbb N,$ we must have some way of proving things about $\mathbb N.$ Finding a proof formalizable in some system like PA or ZFC are the only accepted ways of doing so, although the incompleteness theorem tells us we can't decide every statement in some fixed system.
So what of these "true but unprovable" statements of Godel? How can we determine it's true if it isn't provable? Well, if we're considering the Godel sentence $G$ for PA, we haven't shown it isn't provable, only that it isn't provable in PA. The proof that the Godel sentence is true is done in a stronger system than PA. The basic argument is this: Recall that $G$ essentially says of itself that it is not provable in PA. Now, assuming PA only proves correct things (i.e. it is sound), we can see that it can't be provable in PA, and thus that it is true (since it says it is not provable in PA). It turns out the premise of soundness can be weakened to just consistency.
Godel's first theorem "if PA is consistent, then $G$ is not provable in PA" can be shown in a fairly weak system. The first step toward proving $G$ by the logic above is showing PA is consistent and a closer look reveals this must be the step at which PA fails (this is Godel's second theorem). However, you can prove PA is consistent in ZFC, and the easiest way to do this is to show that $\mathbb N$ is a model for PA. Then the rest of the reasoning falls into place, and proceed to prove $G$ is true. You believe this since your reasoning is formalizable in ZFC and you believe ZFC (or the fragment you used, anyway).
So semantics are not some black box that generates truths that you cannot get from formal proof. Philosophical worries notwithstanding, the truths are there, but there's no way to see what they are without proof. Instead, ZFC is a formal system that proves some things that you cannot prove in PA. And ZFC is also incomplete: in order to believe that its 'true but unprovable statements' (like its Godel sentence or Con(ZFC)) are in fact true, we need to believe assumptions beyond those made in ZFC.
Best Answer
It is of course unsurprising that there are incomplete theories. The surprising bit is that every formal number theory is incomplete - or rather:
Each hypothesis is necessary. There are plenty of natural, interesting theories which are complete, consistent, and reasonably simple - they don't let us "interpret arithmetic," though. Similarly, and more seriously, this implies that for example the true theory of arithmetic - that is, the set of all true statements about natural numbers that can be expressed using $+,\times$, Boolean operations, quantifiers, variables, and parentheses - is not computable (it's obviously complete and consistent and contains basic arithmetic). This may not seem as surprising now, but it means that there are "simple number-theoretic claims" which we cannot hope to prove in whatever axiom system we're using. Put another way: no matter what axiom system we decide to use to study arithmetic, there will be some very concrete statements which we'll never be able to prove or disprove.
Now, I do think that the incompleteness theorem is much less surprising in the modern light of computers, where we have a better sense of what "basic arithmetic" can actually do in terms of logical complexity; indeed, I think other basic theorems are far more surprising. But there's no question that it's hugely surprising insofar as we adopt the principle "all mathematical problems can be satisfyingly solved" in too naive a fashion (we have to be very flexible about what "satisfyingly solved" means to not get ruined by Godel), and this was something that many mathematicians were guilty of from time to time (to put it mildly).