8
$\begingroup$

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?

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ 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. $\endgroup$
    – Marc Hoyois
    Commented Feb 29, 2012 at 13:17
  • $\begingroup$ Also the "metalogic" is a metalogic of itself (as a chain of metalogics on above the other). $\endgroup$
    – Buschi Sergio
    Commented Feb 29, 2012 at 13:26
  • 1
    $\begingroup$ Thank you very much!you say metalogic is obviously true.then,what is it?finite combinatory ? or Intuitionism?or something the computer can verify? $\endgroup$
    – user21284
    Commented Feb 29, 2012 at 14:59
  • 1
    $\begingroup$ some metatheorem‘s proof are very obvious,so I have to believe them.but for example, before The Deduction Theorem(metatheorem) is proved , we do not use it to develop logic theory , when we prove metatheorem increasingly , our meta-language become more abundant , until we build formal set theory , I think we can use zfc as a meta-language to study semantics ,for example compactness theorem requires the concept of cardinal numbers .In this way, circular does not exist .In all this the first , what is the metalogic we recognize it. $\endgroup$
    – user21284
    Commented Feb 29, 2012 at 17:46
  • 1
    $\begingroup$ Thank you very much!I admit that my argument is wrong on the Deduction Theorem，If in accordance with what you said， metalanguage is the same throughout.semantics is based on zfc,then,the first order logic will restated in zfc( you said ：You can formalize all those results within ZFC if you like），then,there are two logic theory,one is preceded zfc,the other is in zfc.so,I think the metalanguage has been replaced with zfc , in the study of semantic. $\endgroup$
    – user21284
    Commented Mar 1, 2012 at 10:07

3 Answers 3

Reset to default
8
$\begingroup$

If I want to prove that two formal languages are equivalent in some respect, aren't I presupposing a "background" formal language?

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:

Overall, a computer system is constructed inductively as a (finite) tower of interpreters, from the micro-code all the way up to the graphical user interface. Compilers and partial evaluators were invented to collapse interpretive levels because too many levels make a computer system impracticably slow. The concept of meta levels therefore is forced on computer scientists: I cannot make my program work, but maybe the bug is in the compiler? Or is it in the compiler that compiled the compiler? Maybe the misbehaviour is due to a system upgrade? Do we need to reboot? and so on. Most of the time, this kind of conceptual regression is daunting even though it is rooted in the history of the system at hand, and thus necessarily finite.

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.

Improve this answer
$\endgroup$
4
$\begingroup$

The issue of language/metalanguage and logic/metalogic seems easy to grasp after a careful study on modern math log textbooks (like Shoenfiled) but it can have (for me) interesting "philosophical" aspects. Please, take a look to Russell & Whithead Intro to their monumental book Principia Mathematica (written 100 years ago): it is a masterpiece of modern mathematics ... but they have the same difficulty with object/meta-logic (see their "explanation" of Modus Ponens). Logic (and mathematics ?) are "language games" : so, we need language (as a tool) to speak about language (an human activity, i.e.an object of the world, to be studied) and we need logic (as a tool) to reason about logic (a mathematical object). The issue (and I think is a big one) comes from the "foundational" aspect that logic receive in the framework of scientific activities. If "fundational" means : start from scratch and build every layer on top of the preceeding one ... I think that last century philosophical debate show us that it is NOT possible to start from scratch at all.

Improve this answer
$\endgroup$
3
$\begingroup$

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$".

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ I understand what you mean , the meta-language can be converted under certain restrictions for the object language , I understand this . My question is whether we can use only the object-language-theorems under the syntax rules(without metathorems ,although you can use the meta-language to describe) ,to build set theory and the whole mathematical. If so,the ZFC which is so established can be used as the background language .the background language can be used as metalanguage for compactness Theorem . if the establishment of set theory need some metatheorem , then we must inquire metalogic. $\endgroup$
    – user21284
    Commented Feb 29, 2012 at 10:32
  • 1
    $\begingroup$ I understand the use of metalanguage is necessary to void paradox,the books I have finded all used some metatheorems to bulid first order logic,is it necessary? after all，the use of metalanguage and the use of metatheorem is different,we can use metalanguage to describe Modus ponens rules,but I think we should not use metatheorem to build the internal theorem of predicate logic. $\endgroup$
    – user21284
    Commented Feb 29, 2012 at 10:46
  • $\begingroup$ Maybe you've been reading the wrong books. If I can make a suggestion, pick up Shoenfield's book "Mathematical Logic". It's 50 years old but I have yet to find a better introduction to formal logic. $\endgroup$
    – Marc Hoyois
    Commented Feb 29, 2012 at 13:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .