Jtdylktuy

What is the difference between the logical formula $alpha$ and expression "$alpha$ is true"? I feel that there is a difference between those expressions. I think this difference is the difference between the language and the meta language. Am I right?

Is there a formal definition of meta language? And do we use our daily language as a meta language when studying logic?? I am very confused. Please help me.

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(xcdot 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(xcdot 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.)