An argument, as intended in the page you mentioned, consists of a collection of premises, used to establish the truth of one (or more) conclusion.
If you were to model this in, say, propositional logic, you would call the premises $p_1, \dotsc, p_n$ and the conclusion $c$.
Then, the argument would be encoded by the formula
$$
p_1 \land \dotsb \land p_n \implies c
$$
To attach a semantic meaning to this formula, i.e. if we want to establish if it is true or false, we need two ingredients:
- The truth values of $p_1,\dotsc,p_n$ and $c$ - you need to fix such values to obtain the truth value of the whole formula; the way you assign this truth values gives you an interpretation.
- A "meaning" for the logical connectives. This means, for example, that the truth value of the conjunction $\land$ can be computed by means of a function (and same goes for the implication).
If we call our interpretation $I$, we say that a formula is satisfied by $I$ (or true under that interpretation) if by assigning the truth values of all the variables as specified in $I$ and then computing the truth values of the logical connectives, the output is true.
As a mathematical convention - this is how implication is defined - a formula of the form $A \implies B$ is false when $A$ is true and $B$ is false; in all the other cases, it is true.
This means that, if the premise $A$ is false, the overall formula is true, no matter the value of $B$. But if $A$ is assumed to be true, then $B$ must be true for the argument to be true.
This means that for an argument to be valid you must be free to give any possible value to each of your variables and still obtain a true formula.
This can be generalized to arbitrary formulas (not only the one in argument form), and that is what the concept of tautology is about.
As an example, the formula $p \lor \neg p$ is a tautology: here, you only have two possible interpretations, one that makes $p$ true, the other makes $p$ false.
You can choose any, and the formula turns out to be true.
Another example of a valid argument is $p \implies p$: assume that something is true; then, that thing is true. Here, you can again choose between two interpretations and no matter what your choice is, the formula is true.
According to the language you are using, there are different ways of defining formula and truth values. You can distinguish between propositional formulas (the ones described above), first-order formulas (as an example, $\exists{x}. p(x) \implies q(x)$), modal formulas and many others. You can choose how many truth values are there: true and false, or true, false and unknown, or infinitely many.
Depending on the choices that you make here, the notion of truth and validity change. Above, I introduced the ones related to classical propositional logic.
You've done a good job of explaining the main differences. A couple of comments:
$\vdash$ is "syntactic consequence", e.g. if we have $a \vdash b$ it means if we've written down $a$ as something we know, we can immediately write down $b$ as something we know.
I would clarify further that it's less about knowledge and more about proof. $a \vdash b$ is true if there is a valid proof of $b$ from $a$, so it's relative to whatever we have decided "valid proof" means. For example, some philosophers and logicians have insisted on denying certain types of proofs and have proposed very restrictive logical systems where you are restricted in when you can deduce $b$ from $a$. In some such systems, $b$ may follow semantically from $a$ ($a \vDash b$) but there may be no way to prove it (so $a \not \vdash b$).
Concretely, some logicians deny that $\lnot \lnot a \vdash a$ -- they aren't willing to accept $\lnot \lnot a$ as a proof of $a$. So it may be that in every world where $\lnot \lnot a$ is true, $a$ is true (semantically), that is $\lnot \lnot a \vDash a$. But if you insist on a standard of proof where $\lnot \lnot a$ is not a good proof of $a$, then $\lnot \lnot a \not \vdash a$.
$\vDash$ is "semantic consequence" ... However I don't know if this is necessarily just a "true"-only thing. It seems conceivable that we could make one for falsehoods too, i.e. if $a \vDash b$ might mean if $a$ is always false then $b$ is always false, of if $a$ is always "dog" then $b$ is always "dog", etc. But I am unsure of this one.
Your speculation here is a bit inaccurate. $a \vDash b$ usually means some variant of "in every possible world where $a$ is true, $b$ is also true". The definition doesn't consider worlds where $a$ is false. And there are no words where $a$ is always "dog" -- $a$ is some sentence, so it is only ever true or false. Calling $a$ a dog would be a sort of semantic mismatch. Maybe $a$ is some fact about dogs, but not a dog itself.
Do I have the right idea so far?
Yes, and let me comment on one thing. In logic, we insist on being extremely formal and distinguishing between things that have different definitions, even if they ultimately amount to the same thing. For example, we distinguish between $(\lnot a) \land (\lnot b)$ (not $a$ and not $b$) and $\lnot (a \lor b)$, even though these ultimately end up being equivalent.
So it is with $\vDash$, $\vdash$, and $\to$. We insist on distinguishing between them because they are defined differently -- and you have summarized the different definitions well. However, there are important senses in which they are all equivalent. In particular, you will probably prove some theorems like:
(Soundness) If $a \vdash b$, then $a \vDash b$.
(Completeness) If $a \vDash b$, then $a \vdash b$.
(Provability of implication) If $a \to b$ is provable -- that is, if $\vdash (a \to b)$ -- then $a \vdash b$. Similarly, if $a \vdash b$, then $\vdash (a \to b)$.
So, all three of them end up being equivalent concepts in the end, but it is important to keep them mentally distinct. There are even some (generally faulty) logical systems where the three concepts are not equivalent, so you have to be careful to not assume they are the same until it is proven.
Best Answer
We may follow Wiki's entry carefully [emphasis added]:
Things are different for the so-called non-classical logic.
See e.g. Intuitionistic Logic :
According, for example, to Brouwer–Heyting–Kolmogorov interpretation the "correct" interpretation of Intuitionistic logic is in term of proof (instead of truth-value).
As discussed before, in the context of classical propositional logic,
But also for classical logic we may have different kind of interpretations, like the algebraic models.
In conclusion :
NO.