Difference about defined symbols in metatheory or in object language

Question

Let me give an example:

1. 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.

Answer 1

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.