## Relation between Metalanguage and Object Language

first,I think we can avoid set theory to bulid the first order logic , by the operation of the finite string.but I have The following questions:

How does "meta-logic" work. I don't really know this stuff yet, but from what I can see right now, meta-logic proves things about formal languages and logics in general. But does it use some logic to do so? Like if I want to prove that two formal languages are equivalent in some respect, aren't I presupposing a "background" formal language? And won't my choice of a "background" (meta) language affect what I can and can't demonstrate? For example, what logic was Godel using when he proved his famous theorems? Was it a bivalent one? A three valued logic? etc

In short,I'm still not sure how reasoning about all possible formal languages work. For example, suppose I say something of the form "for all formal theories, F, if F has property X, then F must have property Y". If I wanted to prove something like that, how does such very general reasoning work? What I mean is that in such a proof, what kind of logic would be employed (for example, would it be a two valued logic?), and does the choice of logic affect the outcome? Do logicians agree on some kind of meta-meta logic, which they use to reason about absolutely everything? Or do they just choose their favorite one?

if metalogic is just predicate logic,It seems circular to me! we build the theory of predicate logic by using predicate logic?For example, in proving some theorem in the object language we seem to assume that it is already correct (in the metalanguage). Or defining some connective in the object language, we use that connective in the metalanguage to do so. It's like they're saying "Alright guys! We are going to prove a bunch of stuff about logic! Oh, by the way, you have to take all this stuff we are about to prove for granted, but don't worry, that's just the "metalanguage"." Something about this seems wrong to me. Maybe I have misunderstood?

-
 Metalogic is not formal. It's just natural reasoning that is obviously true. You have to accept that there is such a thing, or else nothing you say ever makes sense. A proof of a statement of the form "for every formal system F blah blah blah" will be such that, whenever you actually consider a concretely given formal system F, it will convince you that "blah blah blah" is true for that system. If "blah blah blah" says that some formula of F is a theorem, then you will be able to apply the proof to write down a derivation of that formula on a piece of paper. – Marc Hoyois Feb 29 2012 at 13:17 Also the "metalogic" is a metalogic of itself (as a chain of metalogics on above the other). – Buschi Sergio Feb 29 2012 at 13:26 Note similarity to this question: mathoverflow.net/questions/53673/… – Steven Landsburg Feb 29 2012 at 13:34 Thank you very much!you say metalogic is obviously true.then,what is it?finite combinatory ? or Intuitionism?or something the computer can verify? – unknown (google) Feb 29 2012 at 14:59 How about it's just true? Do you not believe things can be true? We could be more helpful if you gave an example of a statement in logic that you find problematic, and explained why. – Marc Hoyois Feb 29 2012 at 15:54
There are two roles for metalanguage: First, to avoid contradictions like the liar paradox, because in the liar paradox we have a statement that speaks about itself so it does not respect the hierarchy language-metalanguage. The other role is to allow us to speak freely and to use theorems of the language as meta-theorems. So if we use the scheme of deduction using the principle of excluded middle, we know that we are using a meta-theorems, but this is just a way to use the corresponding theorem in the object language without repetition. So for example the metatheorem: "If the negation of a proposition A does not hold, then A holds" can be replaced by the theorem in the object language " $\neg \neg A \Rightarrow A$".