is it true that being formulated in metalanguage is a sufficient condition for a statement to belong to metalogic?
Not exactly. Consider the following example : an English book about Greek grammar is about a language : Greek, and it is written in English, the metalanguage. But it is not logic nor about logic.
But, yes,
the distinction between language and metalanguage strictly parallel the distinction between logic and metalogic.
See S.C.Kleene, Introduction to metamathematics (1952), page 62 :
To Hilbert is due the emphasis that strict formalization of a theory involves the total abstraction from the meaning, the result being called a formal system (or sometimes a formal theory); and second, his method of making the formal system as a whole the object of a mathematical study called metamathematics or proof theory.
In dealing with a particular formal system, we may call the system the object theory, and the metamathematics relating to it its metatheory.
We have that metamathematics is the mathematical discipline that studies the properties of those specific mathematical objects that are the formalized theories.
When the formalized theory is a logical calculus, like e.g. propositional calculus or predicate calculus, the metamathematical discipline studying them can be quite obviously called : metalogic.
This is consistent with what G.Hunter asserts in the Preface (p.xi) :
The main contents are : Proof of the consistency, completeness and decidability of a formal system of standard truth-functional propositional logic. The same for first-order monadic predicate logic.
Considering specific examples, we have that :
(1) $p \to q$ is a formula of propositional calculus, i.e. an expression of the object language, written using the symbols of the language, like $\to$.
$\vDash (p \to p)$ is a statement in the metalanguage, asserting that formula $(p \to p)$ is valid.
The symbol $\vDash$ is not part of the calculus, i.e. is not part of the object language. It is a metalinguistic expression.
Regarding (2): exactly; a mathematical logic textbook is "made of" very few parts written in the object language : basically, only the initial examples of formulas and derivations, aimed at showing "how the calculus works".
The main part of the book is "metalogic" : it is metalogical the description of the syntax of the formal system. It is metalogical the proof of theorems like the Deduction Theorem and the Soundness and Completeness Theorems, i.e. the mathematical theorems expressing the properties of the formal system.
In conclusion, regarding (3): yes, a mathematical logic book is a metalogic book.
Compare with a textbook named "Physics": it is a book stating the physical theory, i.e. the theory regarding the facts of the physical realm.
A term is a "name": variables and constants are terms.
In addition, "complex" terms can be manufactured using function symbols.
Example: $n$ is a variable, $0$ is a constant and $+$ is a (binary) function symbol.
Thus, $n,0$ and $n+0$ are terms.
Formulas are statements.
Atomic formulas are the basic building blocks for manufacturing statements.
They are formulas that have no sub-parts that are formulas.
They are manufactured using predicate symbols, like e.g. $\text {Even}(x)$, equality and terms.
Thus, $\text {Even}(n), 0=0$ and $n+0=n$ are atomic formulas.
With connectives and quantifiers we can write more complex formulas, like: $\forall n (n+0=n)$ and $0=0 \to \forall n (n+0=n)$.
Expression can be a "generic" category: it may mean a string of symbols.
We may call well-formed expression a string of symbols that satisfies the rule of the syntax.
If so, it is either a term or a formula.
Best Answer
Yes, as Mauro has commented, your thinking is correct. $\alpha$ is a sentence in some formal language and "$\alpha$ is true" is a statement about this sentence that we make in the metalanguage. To make this precise, we need a notion of what "true" means. This is generally given by a formal interpretation of the language. In general, there are many interpretations of a given language, and truth of a sentence can vary from interpretation to interpretation. As a basic example, consider the sentence $ \exists x(x\cdot x +1=0)$ in a language with symbols $+,\cdot,1,0,$ as well as the symbols of first order logic. When you give all of the symbols the obvious interpretations, this expresses that a square root of $-1$ exists. So this will be true when interpreted in the complex numbers, and false when interpreted in the reals (or rationals, or integers, etc).
To be even more precise, we need to flesh out exactly what truth in a given interpretation means mathematically. For standard semantics of first order languages, the interpretations are structures, and truth is defined inductively on the formulas via Tarski's definition.
In answer to your question about what the meta-language is, it is any language we happen to be using to talk about the formal logical system. So, yes, generally our metalanguage is just our daily 'mathematical English' (or whatever natural language we're using). But notice above I kept saying 'to make this more precise...'. We want to make rigorous mathematical assertions and proofs about sentences, like Tarski made "$\alpha$ is true in interpretation $\mathcal M$" rigorous.
Now, when we mathematically prove "$\alpha$ is true in interpretation $\mathcal M$," we might reasonably wonder where we proved this statement. In other words, can we translate this proof into a formal logical proof, and if so what were the axioms and rules of inference we used? If we succeed in our translation, we can consider (some part of) the metalanguage to be a formal language, and the proof to be carried out in a formal metatheory. For instance, in our above example, we might construe "$\exists x(x\cdot x +1=0)$ is false in $\mathbb R$" as a statement formalized and formally proven in an axiomatic set theory or second order arithmetic.
This all leads to a natural question of whether we can talk about truth of a statement in a given interpreted formal language in that same language. Tarski's famous "'Snow is white' is true if and only if snow is white" can be written $$ T(\ulcorner \phi \urcorner)\leftrightarrow \phi$$ where $\ulcorner \phi \urcorner$ is a formally defined object in the language representing the sentence $\phi$ in the theory, and $T$ is a predicate. Such a $T$ that makes this true for all $\phi$ (for a given way $\ulcorner \urcorner$ of encoding the formal language), is called a truth predicate for the interpreted language. Truth predicates are self-referential by nature and thereby potentially susceptible to paradoxes. In fact, Tarski's theorem tells us that under many circumstances, paradoxes do sink the ship and the truth predicate for a language cannot be defined in the language itself. (This should not be misconstrued as to say it cannot be defined mathematically at all.)