A working knowledge of elementary logic, in Kelley's sense, is a matter of the kind of proficiency with informal deductive reasoning that you pick up early in your mathematical career (and elsewhere of course). E.g., understanding how to refute a proposition by assuming the opposite and deriving an absurdity, understanding how to establish a universal generalization by working with an arbitrary instance, understanding how to establish a conditional by supposing the antecedent is true and deriving the consequent.
Formal logical systems, where we carefully define the syntax, carefully define what can be inferred from what, etc., aim to regiment and formalize such patterns of informal deductive reasoning: as Kelley says, the exercise of regimenting can indeed be illuminating about our ordinary reasoning.
A formal mathematical theory (or system) is what you get when you take a formal logical system and add some specific mathematical axioms, and thereby regiment an informal mathematical theory.
(Metalogic is another step further, being the informal mathematical investigation of such formal logico-mathematical systems treated as themselves objects of mathematical interest)
I see that valid formula (proposition or statement) is the one that is valid under every interpretation. But this is a tautology. Is there any difference between tautology and valid formula?
Some people use "tautology" in logic in a wide sense, to mean any logically true wff. But others use "tautology" more narrowly to mean true in virtue of truth-functional structure (so, "valid by the truth-table test"). So, for example, $\forall xFx \to Fa$ would count as a tautology in the first, wide, sense but not in the second, narrow, sense. (How to use 'tautology', then, is a matter of terminological preference: I much prefer the second narrower usage as it gives us a label for a special class of logical truths which we need a label for.)
They also say that $A, B \vDash \Phi$ is valid if it preserves the truth
No they don't. Or at least, they shouldn't. It is the inference that preserve truth. Thus if $A, B \therefore \Phi$ necessarily preserves truth, then it is valid. But $A, B \vDash \Phi$ is not an inference: it is a meta-linguistic statement about the inference, and says the inference is valid.
They also say that in addition to being valid, i.e. preserving the truth, your argument is sound when premises are also valid.
Fine: an argument is sound if it has true premisses and a valid inference move.
But there is another definition of soundness, which tells that theory is sound if formula provability implies that formula is semantically valid.
As you almost say, this is a definition of what it is for a formal deductive system to be sound.
Arguments aren't formal deductive systems, and soundness for arguments is not soundness for formal deductive systems. The notions can't be identical. But there is some similarity between the two notions -- both have something to do with being trustworthy (an argument won't lead you astray about the truth if it starts with truths and proceeds by truth-preserving moves, i.e. is sound; likewise a formal system encoding inferences won't lead you astray about what's a valid inference if it is sound)
Best Answer
Usually in logic correctness is a property of sequences/trees of formulas/sequents (depending on the system considered) that express they are valid proofs: that is that they are sequences/trees which are build applying the inference rules of the logic considered.
Soundness is a property of a logic, where by a logic we mean a proof system (i.e. a set of inference rules) and a semantics, basically a logic is sound if every time we have $T \vdash \varphi$ (that is $\varphi$ can be proved by the inference rules from the formulas in $T$) we also have that $T \models \varphi$ (that is $\varphi$ is true in every model of $T$).
So correctness is a concept that belongs to the syntactic setting while soundess links syntax with semantics.
Of course there are other possible use of the term correctness but these use belongs outside the realm of logic (or at least I cannot think of other uses of the word in logics).
Hope this helps.