Is my intuition for ${\vdash}$ and ${\models}$ correct? I just want to check my idea for what exactly is meant by ${\vdash}$ and ${\vDash}$ is correct (I am a noob to logic).
${S\vdash t}$ means "$t$ is provably true using finitely many elements of $S$ within that system", whereas ${S\vDash t}$ means "$t$ is true given $S$", but doesn't make any statements about whether we could prove it within that system $S$. Is this essentially correct? Thank you.
 A: I don't think you have it quite right.

"$S\models\varphi$" is defined purely semantically: it means "If $\mathcal{M}$ is a structure satisfying each sentence in $S$, then $\mathcal{M}$ satisfies $\varphi$ as well." In particular, this notion is secondary to the notion of a sentence being true in a structure (which uses the same
"$\models$" symbol, incidentally).
Meanwhile, "$S\vdash\varphi$" is not actually fully precise! It really only makes sense once we specify a proof system $\mathfrak{P}$. This is a totally different object from $S$ and $\varphi$; basically, it's just a set of rules for deriving sentences from sets of sentences. If we can derive $\varphi$ from $S$ via $\mathfrak{P}$, we write "$S\vdash_\mathfrak{P}\varphi$."
A priori these are two totally different things, and we can whip up silly "proof systems" which are obviously unrelated to the semantics: e.g. "bogus ponens," the proof system which lets you deduce anything from anything.
(Note that I haven't defined "proof system" precisely - nor am I going to. There are various definitions floating around in the literature, with no one particular one being universally accepted. And there are further subtleties which can emerge, see e.g. here.)

So how are these connected, and why do we abuse notation by writing "$\vdash$" instead of "$\vdash_\mathfrak{P}$?"
Well, it turns out that for a wide variety of $\mathfrak{P}$s we in fact have soundness and completeness of the proof system with respect to the semantics, that is, $$S\vdash_\mathfrak{P}\varphi\quad\iff\quad S\models\varphi$$ (the left-to-right direction is soundness, the right-to-left is completeness - and it's the latter which is by far the more interesting direction). Moreover, since we're specifically interested in the semantics above, proof systems which are not sound and complete aren't generally of interest.
This means that we can usually write "$\vdash$" without fear of serious confusion, since all the "reasonable" proof systems we look at will behave identically here. But in other contexts, and for certain questions (like questions about proof length), the specific proof system may matter a lot. So when first learning this stuff it's a good idea to fix a single proof system from the get-go, and only generalize later once the basics are understood.
