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?
Best Answer
Yes -- but the distinction between object language and meta language can be studied carefully. This is an important part of proof theory, as well as (in a more modern context) of the theory of programming languages. Let me quote from Olivier Danvy's entry on "Self-interpreter" in the appendix to Jean-Yves Girard's Locus Solum:
In this view (in contrast to the views expressed in some of the other answers), the meta language does not have any special status: it is distinguished from the object language by its role rather than by its character. In particular, a meta language $L_1$, used to interpret some object language $L_2$, may itself be the object language of some interpretation in $L_0$.
On the other hand, often both mathematicians and computer scientists are interested in keeping the meta language as minimalistic as possible, simpler than the object language in some sense. A paradigmatic example is Gentzen's cut-elimination argument, which proves the consistency of first-order Peano arithmetic (PA). If the meta language for this proof is taken to be ZFC, then the result seems vacuous, since ZFC already includes PA (indeed is much more complicated than PA). However, in fact only a very small logical fragment of ZFC is needed to formalize the proof, namely PRA + $\epsilon_0$ (primitive recursive arithmetic plus transfinite induction up to $\epsilon_0$). Although PRA + $\epsilon_0$ is not included in PA (so that Gentzen's theorem does not contradict Gödel's), neither is PA included in PRA + $\epsilon_0$, since the latter only allows (transfinite) induction on quantifier-free statements. This is what prevents Gentzen's argument from being "circular", and the sense in which it reduces a statement about the object language to a "simpler" meta language.