How to verify satisfialibility in a model? (Confusions with Gödel's Completeness Theorem)

I would say you are right - there is no reason to expect Goedel's completeness theorem to be true!

Except for the proof.

I consider the completeness theorem to be the most counterintuitive result in basic logic, far more so than the incompleteness theorem (whose surprisingness is in fact debatable. As you say, it shows that a very concrete statement "$T\vdash \varphi$" is equivalent to a seemingly-much-more-complicated statement "Every model of $T$ satisfies $\varphi$", and the complexity of the latter is suggested by the fact that, for fixed $M$ and $\varphi$, the question "Does $M\models\varphi$?" is in general of very high complexity.

One way to think about what happens is this: telling whether every model of $T$ satisfies $\varphi$ can be easier than telling if a specific model of $T$ satisfies $\varphi$. Specific models can be quite complicated; however, every theory will also have models which are "reasonably simple" (see below for more on this). These models will often be unnatural, but they exist, and they bear on the question of whether $T\models\varphi$; and it is these models, essentially, that make the question an answerable one.

Having acknowledged that GCT is counterintuitive, let me now try to convince you that it's true.

Let's think about the contrapositive: that if $T\cup\{\neg\varphi\}$ is consistent, then we can build a model $M$ of $T$ with $M\not\models\varphi$. Note that this makes our job much easier - we only have to build one model! And even though the general problem "Does $N\models \psi$?" is extremely complicated, the specific question we're interested in ("Does $M\models\varphi$?") may not be so bad.

Here's the natural construction to look at: take the set of terms in the language of $T$, and "mod out" by $(T\cup\{\neg\varphi\})$-provable equivalence. E.g. in an appropriate theory of arithmetic, "$1+1$" and "$(1+1)\times 1$" are terms which are provably equal, so they represent the same equivalence class. It's not hard to show that the operations and relations of the language are well-defined on these equivalence classes. So there's a natural structure assigned to the theory $T\cup\{\neg\varphi\}$; if you think about it for a bit, it should become plausible that this is in fact a model of $T\cup\{\neg\varphi\}$!

. . . Of course, it's not, though. The proof isn't that simple. But the idea is right, it just needs some work. Some of this work involves improving the theory $T\cup\{\neg\varphi\}$ itself ($T\cup\{\neg\varphi\}$ might not "decide" certain important questions; alternatively, the language of $T\cup\{\neg\varphi\}$ might not "have enough terms" to build the structure we want); the other part of the work involves working with the specific properties of the provability relation "$\vdash$". (See e.g. these two questions, respectively.)

Computability-theoretic aside: "simple" models. (No, I don't mean that kind of simplicity.)

While the completeness theorem lives solidly in model theory, interesting things happen if we bring computability into the picture. The proof of the Completeness Theorem gestured vaguely at above is a construction of a model. It's not hard to see that it is not a computable construction in any good sense, but that's not the end of the story: we can ask how noncomputable it is.

It turns out that it is actually surprisingly close to computable - namely, we have:

Suppose $T$ is a countable theory in a countable language. Then there is a model of $T$ which is low relative to $T$.

Here, "low" is a computability-theoretic property: a set $X$ is low if the halting problem defined relative to $X$ is no more complicated than the classical halting problem. Lowness relative to $A$ is defined similarly. By comparison, the question "Does $T$ prove $\varphi$?" is at the level of the halting problem relative to $T$; so actually, we're building a model that is much simpler than the original provability question!

And set theory has things to say too.

By reducing everything to finite combinatorics, the completeness theorem shows that questions like "Does $2^{\aleph_0}=\aleph_1$?" will never arise when trying to tell whether every model of of some theory satisfy some sentence. But this is just a result about first-order logic! For general logics, set-theoretic issues can indeed crop up.

A great example of this is second-order logic (with the standard, as opposed to Henkin, semantics; the Henkin semantics makes it essentially equivalent to first-order logic). Second-order logic allows you to quantify over relations and functions on the domain, in addition to individuals (which is what first-order logic lets you quantify over). For instance, there is a second-order sentence true in exactly the infinite structures: it looks like "There is an injective, non-surjective function," or more formally $$\exists F[\forall x, y(F(x)=F(y)\implies x=y)\wedge \exists z\forall x(F(x)\not=z)].$$ So Compactness immediately fails for second-order logic. But the one that takes the cake is:

There is a sentence $\chi$ in second-order logic, which is a validity (= true in every structure) if and only if the Continuum Hypothesis is true.

This takes a bit of work to prove; if you're interested, I'll add its construction in detail.

My point is that set-theoretic issues do indeed come up when trying to analyze the satisfaction relation for arbitrary logics; but the completeness theorem shows that first-order logic is especially nice. And this is, indeed, a very nontrivial fact!

If you're interested in comparing first-order logic with other logics, you may be interested in abstract model theory!

Notice that the right side says "for every model $\mathcal{M}$". If something is undecidable, then it will be true for some models and false for others. So the right side fails, and so does the left side, i.e., there is no formal proof of an undecidable statement in first-order logic. This is all as expected.

I see the problem cause in some models $(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$ may be undecidable.

I think you are confusing provability with satisfaction, since for any particular model a sentence will always either be true or false. Undecidability applies to provability, since it may be the case that a sentence is true in some models and not others.

We can end up with set theoretical situation $\mathfrak{c}=\aleph_1$. One cannot tell if this hold or not.

We can tell if it holds for some particular model. Remember that Godel and Cohen together showed that CH holds in some models of ZFC and not others. Completeness simply says that this one fact is enough to prove that CH is independent of ZFC.