1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ This is essentially repeating part of Emil's answer, with explicit reference to this part of the question: "... seem to imply that all of theorems of object theory can be described in metatheory". Indeed, the fact that something is a theorem of the object theory is itself a metatheoretic fact. $\endgroup$ – Andreas Blass Feb 10 '12 at 14:53
  • $\begingroup$ sorry,"relation" in my depiction is "formula". in fact,I want to know the difference of the following sentences 1)let A,B are formulas ,if A is provably then B is provably. 2)let A,B are formulas ,(A→B) is provably $\endgroup$ – user21284 Feb 10 '12 at 14:59
  • 2
    $\begingroup$ There's a big difference between "(provably A) implies (provably B)" and "provably (A implies B)". For example, Gödel's second incompleteness theorem says that, when "provably" refers to a sufficiently strong theory T, if "T is consistent" is provable, then so is "0=1". On the other hand, for reasonable T, "if T is consistent then 0=1" (in other words, "T is inconsistent") will not be provable. $\endgroup$ – Andreas Blass Feb 10 '12 at 16:49
  • $\begingroup$ 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)↔(The translations of the reflexive, symmetric, and transitive properties in the formal language)] I want to know the difference between these two statements. $\endgroup$ – user21284 Feb 11 '12 at 4:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.