Difference about defined symbols in metatheory or in object language  Let me give an example:


*

*this is a definition in object language:
R(x,y) is a symmetric formula  ↔ （∀x∀y(R(x,y)→R(y,x))）


2.this is a definition in metatheory:
R(x,y) is a symmetric formula   if and only if R(x,y)→R(y,x) is a theorem.
In other words:
R(x,y) is a symmetric formula   if and only if ⊢ R(x,y)→R(y,x).
In other words:
R(x,y) is a symmetric formula   if and only if ⊢∀x∀y(R(x,y)→R(y,x))
I have the following questions:
1. These two definitions seem to imply all of  theorems of object theory can be described in metatheory,Is that so ? How to precise state and prove this translation process for every theorem?
2.Our everyday reasoning in mathematics , in the end is in the object language or in the meta-language ? 
another example:
I have seen a paragraph of text:
Thus, in the metatheory “P : A → A is an equivalence relation” means that “P ⊆ A × A and P is reflexive, symmetric, and transitive” is true, whereas in ZFC it means that the quoted (quasi) translation is provable (or has been taken as an assumption).
I consider the following words is another definition: ⊢ [(P : A → A is an equivalence relation)↔(P ⊆ A × A and The translations of the reflexive, symmetric, and transitive properties in the formal language)].
I want to know the difference between these two statements.
 A: To begin with the second question, everyday reasoning in mathematics is in the object language. (Though if you happen to be a logician, this object language may well get used as a meta-language for another object language.)
As for the first question, I don’t quite understand the goal. First, the definition of a symmetric relation in the meta-theory is in fact the same as in the object theory (which you didn’t name, btw, so I’ll call it $T$): a relation $R(x,y)$ is symmetric if $R(a,b)$ whenever $R(b,a)$, for every $a,b$. What you described is not the definition of a symmetric relation, but actually the definition of a predicate symbol being $T$-provably a symmetric relation. You can certainly do this transformation with any other formula: if $\varphi$ is a statement of the object language expressing that a property $P$ is true, you can consider the statement $T\vdash\varphi$ of the meta-language expressing that the property $P$ holds $T$-provably. But this is trivial, so I don’t see what you intend to gain by it.
