$A \models B$ means that $B$ is true in every structure in which $A$ is true. $A\vdash B$ means $B$ can be proved using $A$ as the premises. (In both cases, $A$ is a not necessarily finite set of formulas and $B$ is a formula.)
First-order logic simultaneously enjoys the following properties: There is a system of proof for which
- If $A\vdash B$ then $A\models B$ (soundness)
- If $A\models B$ then $A\vdash B$ (completeness)
- There is a proof-checking algorithm (effectiveness).
(And it's fortunately quite a fast-running algorithm.)
That last point is in stark contrast to this fact: There is no provability-checking algorithm. You can search for a proof of a first-order formula in such a systematic way that you'll find it if it exists, and you'll search forever if it doesn't. But if you've been searching for a million years and it hasn't turned up yet, you don't know whether the search will go on forever or end next week. These are results proved in the 1930s. The non-existence of an algorithm for deciding whether a formula is provable is called Church's theorem, after Alonzo Church.
About 1., Gödel's First Incompleteness Theorem is a ingenious exercise of "coding" formal properties and relations regarding a theory $F$ with "a certain amount" of arithmetic inside $F$ itself.
This exercise ends with the definition of the so-called provability predicate $Prov_F(x)$ which holds of $a$ iff there is a proof in $F$ of the formula $A$ with "code" $a$.
To complete the proof, [it is used] the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that
$⊢_F G_F \leftrightarrow ¬Prov_F(\ulcorner G_F \urcorner)$ [where $\ulcorner x \urcorner$ is the "code" of formula $x$].
Thus, it can be shown, even inside $F$, that $G_F$ is true if and only if it is not provable in $F$.
Thus, "reading" the above proof, we can "know of" the truth of $G_F$ (provided that $F$ is consistent) simply because $G_F$ is not provable in $F$ and $G_F$ is equivalent to the formula $¬Prov_F(\ulcorner G_F \urcorner)$.
About 2. :
Why doesn't the fact that $G$ is true constitute a proof of $G$ ?
Because a proof in $F$ of $G_F$ is a precise formal objcet and G's Incompleteness Th shows that such a proof in $F$ cannot exists.
Thus, the conclusion of G's Incompleteness Th is twofold :
For 3. :
By Gödel's Completeness Theorem, there are formal systems in which G is false. How can this not cause a contradiction ?
NO; by G's Completeness Th there are models of $F$ in which $G_F$ is false.
G's Completeness Th, prove that a formula provable in a theory $T$ must be true in all models of $T$.
Thus assuming that $\mathbb N$ is a model of our theory $F$ containing "a certain amount" of arithmetic, we have that all theorems of $F$ (i.e. formulae provable from $F$'s axioms) must be true in all models of $F$.
But $G_F$ is not provable from $F$'s axioms; thus, it must be not true in some model of $F$.
The proof of G's Incompleteness Th give us the insight that $G_F$ is true in $\mathbb N$; thus, it must be false in some model of $F$ different from $\mathbb N$, i.e. in some non-standard model of arithmetic.
Best Answer
The usual way to define truth is due to Tarski. Given a structure $M$ (i.e. a set with operations and relations), we recursively define $M \models \phi$, meaning $\phi$ is true in $M$. For concreteness, let's consider the natural numbers $N = (\mathbb N, +, \times, 0, 1, <)$:
$N \models a + b = c$ if it the output of the binary function $+$ on input $(a,b)$ is $c$. Similarly for $N \models a \times b = c$.
$N \models a < b$ if $(a,b)$ is in the set $\mathord< \mathbin{\subseteq} \mathbb N^2$.
$N \models \phi \land \psi$ if $N \models \phi$ and $N \models \psi$ and $N \models \phi \lor \psi$ if $N \models \phi$ or $N \models \psi$.
$N \models \neg \phi$ if it is not the case that $N \models \phi$.
$N \models \exists x \phi(x)$ if there is some $a \in \mathbb N$ so that $N \models \phi(a)$ and $N \models \forall x \phi(x)$ if for all $a \in \mathbb N$ we have $N \models \phi(a)$.
In other words, truth is defined exactly how you would expect; symbols in the language correspond to certain constants, functions, and relations in the structure and truth is based upon that connection.
Provability, on the other hand, isn't a property of structures. Instead, it's a property of theories. If $T$ is a theory, meaning a set of sentences in some fixed language, then we can define a provability relation $T \vdash \phi$. There are many ways to do the details here to match with our intuitive notion of provability. But the important things are that the provability relation should be closed under valid inference rules (e.g. if $T \vdash \phi$ and $T \vdash \phi \rightarrow \psi$, then $T \vdash \psi$), that the axioms of $T$ are provable (if $\phi \in T$ then $T \vdash \phi$), and that logical validities (statements true in any structure) are provable.
We can now ask about how provability and truth relate. Any definition of provability worth a damn will be sound. This means that if $M$ is a model of $T$ (i.e. every axiom of $T$ is true in $M$, when interpreted appropriately), then $T \vdash \phi$ implies $M \models \phi$. In other other words, if we have proved something, then we know it is true. Moreover, as Gödel showed, first-order logic is complete. This means that if every model $M$ of $T$ has $M \models \phi$, then $T \vdash \phi$.
On a final note, it's very common to see people refer to truth without indicating a structure they are working in or refer to provability without indicating a theory they are working from. In the former situation, it's usually clear what structure is implicitly being used. For instance, the statement "17 is prime" is referring to the natural numbers, and can be translated to a formal statement something like $N \models \forall x < 17\, \exists y \le 17 \ (x \times y = 17 \rightarrow x = 1)$.
In the latter situation, when referring to provability, some implicit background of commonly accepted mathematics is assumed. When we say that the intermediate value theorem is provable, we mean that there is a proof of the IVT from some commonly accepted basic principles.