Formal languages and theories - difference between these two symbols

Question

I am new to formal languages and their theories and I am confused by these two particular symbols: $\models$ and $\vdash$. For example, let's say that we are working with the language of an ordered field:
$$\mathcal L = (\{+, \cdot)\}, \{\le\}, \{0, 1\})$$ where the functions and the predicate are binary. Now, let's also assume that our model is the field of the real numbers and let our theory be the set of the field axioms.
Let's denote our theory by $\mathcal T$. Now, what is the difference between these two notations: $$\mathcal T \models (\forall x)(\forall t)(x \cdot x \le x \cdot x + t \cdot t)$$ $$\mathcal T \vdash (\forall x)(\forall t)(x \cdot x \le x \cdot x + t \cdot t)$$

Answer 1

$\Gamma \vDash \varphi$ means that based on the formal semantics of the symbols involved, it is impossible for all statements in $\Gamma$ to be true while $\varphi$ is false.

$\Gamma \vdash \varphi$ means that we can syntactically derive $\varphi$ from $\Gamma$. So that should really be defined relative to some kind of proof system with specific rules of derivations. That is, if $S$ is such a system, then we can say that $\Gamma \vdash_S \varphi$ if and only if using the rules of derivation of system $S$, we can derive $\varphi$ from $\Gamma$.

We can then also define the impotant notions of soundness and completeness of system $S$:

$S$ is sound iff for any $\Gamma$ and $\varphi$: If $\Gamma \vdash_S \varphi$ then $\Gamma \vDash \varphi$ (in other words, $S$ does not allow you to infer things that don't logically follow)

$S$ is complete iff for any $\Gamma$ and $\varphi$: If $\Gamma \vDash \varphi$ then $\Gamma \vdash_S \varphi$ (in other words, the rules of $S$ are string enough so that anything that logically follows can in fact be derived using the rules in $S$)

Since we typically assume that the formal proof system we are working with is both sounds and complete, we often drop the $S$ from $\Gamma \vdash_S \varphi$ and simply say $\Gamma \vdash \varphi$