Relation between Metalanguage and Object Language

Relation between Metalanguage and Object Language | |

•Adam N
Newbie Usergroup: Members Joined: Aug 02, 2011 Total Topics: 1 Total Posts: 5 |
Posted Aug 2, 2011 - 7:09 PM:
Subject: Relation between Metalanguage and Object Language I've recently started learning some formal logic but one thing has been bugging me. It seems circular to me! 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? Or, in one of the books I have, set theory is used to state and prove things in logic. But I always thought that logic "preceded" set theory in the sense that in set theory, axioms are stated and theorems are proved, using predicate logic. Oh, and another question while I'm at it. 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, (I won't pretend to know anything about Godel's theorem, but) what logic was Godel using when he proved his famous theorems? Was it a bivalent one? A three valued logic? etc... My apologies if I'm rambling but I really love logic from what I've learned so far and sincerely want to know, but this has been driving me crazy. |

•MoeBlee
aka I. Kabruob Usergroup: Members Joined: May 19, 2005 Total Topics: 10 Total Posts: 352 |
Posted Aug 3, 2011 - 2:03 PM:
Adam N wrote: Yes, logicians are aware of your point: Some of the principles in the meta-theory are the same as those formalized in the object theory. I don't see how that can be avoided. Certain basic prinicples, such as modus ponens, symmetry of equality, etc. are so basic that just about any reasoning makes use of those principles. So, even though we wish to formalize those principles in the object theory and, in a meta-theory, prove things about the object theory, we'll have to make use of certain basic principles in the meta-theory, and some of the principles used in the meta-theory will be those that we're formalizing in the object theory. in proving some theorem in the object language we seem to assume that it is already correct (in the metalanguage) Basic situation: Either we have an infinite escalation of formal meta-theories, or we agree to take certain principles unformalized. Adam N wrote: Yes, we recognize that we use formal logic to formalize set theory and then use set theory to prove things about formal logic.set theory is used to state and prove things in logic. But I always thought that logic "preceded" set theory in the sense that in set theory, axioms are stated and theorems are proved, using predicate logic. Again, we can either keep formalizing to higher and higher meta-theories, ad infinitum, or at some point agree to some informal basic logical and set theoretical principles. Personally, the way I do it is as follows: (1) In an informal set theory S as informal meta-theory, formalize a first order logic L as a formal object system. (2) Using L, formalize a formal set theory S*. (3) In S* as formal meta-theory, formalize a formal first order logic L*. Step (3) will be just like step (1), except step (3) is formal where step (1) was informal. After we've done (1)-(3), we could keep going up and up in formal meta-theories, formalizing the one below. But we see that that would be intellectually redundant to do so. The process will be the same each time. Perhaps think of it like a "successor function". For each formal theory, there is a formal meta-theory above it, but the process of going from theory to the meta-theory looks the same each time. |

•Adam N
Newbie Usergroup: Members Joined: Aug 02, 2011 Total Topics: 1 Total Posts: 5 |
Posted Aug 3, 2011 - 9:04 PM:
parameter wrote: After we've done (1)-(3), we could keep going up and up in formal meta-theories, formalizing the one below. But we see that that would be intellectually redundant to do so. The process will be the same each time. Perhaps think of it like a "successor function". For each formal theory, there is a formal meta-theory above it, but the process of going from theory to the meta-theory looks the same each time. Thank you very much! That was very helpful and I think I understand this better now. One thing though: 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? Furthermore, consider your 3-step sketch of how you like to proceed to develop formal logic and formal set theory. Suppose I started with an informal logic where I demanded that that everything is either true or false, and not both. Then formalized set theory as usual. Then someone else started with an eighteen-valued logic and developed some wacky set theory. How would we compare the two approaches? Can we only do so informally? Or is there some formal language which is used to talk about all formal languages (including itself)? Is there a "view from nowhere"? |

•Dantesco
Resident Usergroup: Members Joined: Jul 17, 2010 Location: Brasil Total Topics: 19 Total Posts: 464 |
Posted Aug 3, 2011 - 11:07 PM:
Adam N wrote: Thank you very much! That was very helpful and I think I understand this better now. One thing though: 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? Furthermore, consider your 3-step sketch of how you like to proceed to develop formal logic and formal set theory. Suppose I started with an informal logic where I demanded that that everything is either true or false, and not both. Then formalized set theory as usual. Then someone else started with an eighteen-valued logic and developed some wacky set theory. How would we compare the two approaches? Can we only do so informally? Or is there some formal language which is used to talk about all formal languages (including itself)? Is there a "view from nowhere"? You've raised a deep concern in philosophy of logic. So far I know, there are only two logics such that formalize the same mathematics underlying them: classical logic and intuitionist logic. |

•MoeBlee
aka I. Kabruob Usergroup: Members Joined: May 19, 2005 Total Topics: 10 Total Posts: 352 |
Posted Aug 4, 2011 - 10:31 AM:
Adam N wrote: Usually, we use ZFC (and ZFC is in classical predicate logic) for our meta-theory. But we can, and sometimes do, use different theories (and even different logics), whether formal or informal. 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? Adam N wrote: We can do whatever we want, use whatever theories we wish to use. And some theories do "talk" about themselves in a certain sense. But there is not one "master theory" to talk about all theories.
Suppose I started with an informal logic where I demanded that that everything is either true or false, and not both. Then formalized set theory as usual. Then someone else started with an eighteen-valued logic and developed some wacky set theory. How would we compare the two approaches? Can we only do so informally? Or is there some formal language which is used to talk about all formal languages (including itself)? |

•Spoonwood
Initiate Usergroup: Members Joined: Apr 01, 2011 Total Topics: 0 Total Posts: 57 |
Posted Aug 7, 2011 - 3:02 PM:
I don't agree with MoeBlee on this and (classical) logic doesn't work this circularly. In classical logic proofs of theorems in the object language basically prove that a given *formula* behaves in some way (derivability usually, possibly something concerning truth-values). It comes as key to point out that you've proven things about formulas, or in other language statement forms, or in other terms well-formula formulas (wffs). The way I look at it, the object language consists of nothing but wffs. Even to say "the formula Cpp is a wff" isn't in the object language, but rather *about* the object language, and thus in the metalanguage. The metalanguage has other things like "derivability" and the like. Say you want to prove the theorem CpCCpqq. In other words, you want to prove that the wff CpCCpqq behaves a certain way in the object language, or equivalent comes as a special type of wff in the object language. A natural-deduction style proof of this can go: 1 | p assumption 2 || Cpq assumption 3 || q 1, 2 modus ponens 4 | CCpqq 2-3 conditional introduction 5 CpCCpqq 1-4 conditional introduction Now, isn't CpCCpqq just a way of stating the rule of modus ponens which this proof used? No, and there exist several differences. 1. The rule of modus ponens happens in the metalanguage, while the formula proven above happens in the object language. 2. Consider what each mean in words and how they might go in a symbolization... in words the rule of inference modus ponens ponendo can get written "From some proposition p, along with some proposition Cpq, we may infer the proposition q in the consequent of Cpq." Or in symbols p, Cpq |-q. The formula proven happens in the object language and goes |- CpCCpqq. In words it can go "If p, if, if p implies q, then q." Note that, the rule of inference talks about two propositions *given* from which we may infer a third proposition. Implicitly all three propositions end up of the same type (derivable from the syntactic point-of-view, or true from the semantic point-of-view). The propositions are by no means necessary unified, they just belong to the same category, somewhat like how chimpanzees and gorrilas aren't really unified, but both qualify as apes. The formula proven in the object language necessarily stands as *one, single, unified* proposition. Were they the same, then basically we have 1=3, so they really do differ. 3. From a syntactic point-of-view the formula proven necessarily requires a rule-of-inference to get proven, or must get taken as an axiom to qualify as a theorem in some logical system. From a semantic point-of-view the formula proven must have truth value of true. Neither of these need hold true for the rule of inference modus ponens. It simply doesn't have a truth value and it doesn't require anything to get proven. It occurs as a *rule* NOT as a statement, just as the rules of minesweeper are not statements about minesweeper, but rather a means by which the game works, while statements about how many mines occur in a certain patch of squares are not rules about minesweeper, but rather *inferred* in some way. 4. The deduction metatheorem and its converse clearly distinguish "p, Cpq |- q" from "|- CpCCpqq", and relate them together (in classical logic). If the distinction between meta and object language really didn't hold, the deduction metatheorem simply wouldn't make sense pretty much even as a conjecture. |

•chopchop
Resident Usergroup: Members Joined: Jul 12, 2011 Total Topics: 10 Total Posts: 462 |
Posted Aug 7, 2011 - 3:26 PM:
Adam N wrote: I've recently started learning some formal logic but one thing has been bugging me. It seems circular to me! 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? Or, in one of the books I have, set theory is used to state and prove things in logic. But I always thought that logic "preceded" set theory in the sense that in set theory, axioms are stated and theorems are proved, using predicate logic. I think you are confusing the point of the soundness proofs. The goal isn't to prove that logic (as some general thing) is correct. It's to prove that a formal system of deduction does what it should. For instance, in constructing a formal system of deduction, we want to include a bunch of rules that tell us how to get from things like P to things like Q. But we don't want those rules to lead us astray. Specifically, we don't want those rules to take us from "true" to "false." Think of the formal system as something like a computer program. We aren't questioning whether p and if p then q gives us q. What we are questioning is whether our computer program works or not: if we input "P->Q" and "P", does it output Q (as it should) or ~Q (or something else)? And again, no one uses set theory to prove that logic (as a general thing) is correct. That doesn't make sense, since the set theory itself presupposes logic. The set theory is used to model the formal system, to make sure that it works as it should. Adam N wrote: Oh, and another question while I'm at it. 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, (I won't pretend to know anything about Godel's theorem, but) what logic was Godel using when he proved his famous theorems? Was it a bivalent one? A three valued logic? etc... Yes, the "meta-logic" uses its own logic to prove results. If you are interested in this kind of thing, you should look at Gentzen's consistency proof of arithmetic. That's an interesting example of a "meta proof." Adam N wrote: My apologies if I'm rambling but I really love logic from what I've learned so far and sincerely want to know, but this has been driving me crazy. |

•Adam N
Newbie Usergroup: Members Joined: Aug 02, 2011 Total Topics: 1 Total Posts: 5 |
Posted Aug 9, 2011 - 8:06 PM:
Thanks guys for your responses. I've been looking through other discussions on this site, and confusion between object language and metalanguage seems to be quite common, so I think this is worth getting absolutely straightened around in my mind. Tell me if I have: I think my confusion was that I didn't understand what metalogic was supposed to do. It wasn't supposed to justify logic because such a thing doesn't really make sense. We cannot do so, anymore than we can justify the axioms of a vector space, or the definition of a number. Instead we are trying to make it precise, "formal", rule based. Carrying on a bit with the number example, it wouldn't make sense to ask "is my definition of number 'correct'?." But we can ask "does our definition of 'number' do what we want it to?" In particular, does it ensure that all the arithmetical operations can be defined in such a way that all the propositions we want to have, like 2+2=4, come out right. If we defined 'number' and 'addition' in such a way that 2+2=5, there wouldn't be anything necessarily wrong with this, but it just isn't what we set out to do. Similarly, instead of asking meaningless questions like "is our logic 'correct'?", we can ask "does it do what we want it to do?". In particular, we have in mind some idea of what truth is (be it two valued, or otherwise), and we make this notion precise using truth tables, and other such things. Then we can ask questions like: "Are our inference rules truth-preserving?". That is, if we start with a true formula, and correctly apply our inference rules, do we only get more true formulas? "If we can show a formula to be true using truth tables, can we derive it using inference rules?" "What about the other way around?" etc... These are (among) the questions which metalogic seeks to address. Is this right? Did I get it? Edited by Adam N on Aug 9, 2011 - 11:45 PM |

•Phil Scott
Newbie Usergroup: Members Joined: Apr 11, 2004 Total Topics: 0 Total Posts: 0 |
Posted Aug 10, 2011 - 6:44 AM:
Adam N wrote: Metareasoning is generally unformalised, so this isn't 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? really a mathematically meaningful question.But there is a tradition in computer science of using one formal system to reason about another formal system, so you have a formal metalogic and a formal object logic. The metalogics here tend to be typed higher-order logics, with lots of facilities for constructing recursive definitions and doing structural induction, so you can easily and reliably define and reason about the syntax of the object logic. Can we only do so informally? Or is there some formal language which is used to talk about all formal languages (including itself)? Is there a "view from nowhere"? There's only so much reasoning that a logic can do about itself. In particular, it can't establish its consistency, or various consequences of its consistency.I think my confusion was that I didn't understand what metalogic was supposed to do. It wasn't supposed to justify logic because such a thing doesn't really make sense. We cannot do so, anymore than we can justify the axioms of a vector space, or the definition of a number. Instead we are trying to make it precise, "formal", rule based. Think of a formal system as an ordinary mathematical object, like one of your favourite algebraic structures, or a particular kind of function. The problem is then just ambiguity.For instance, I have a bunch of objects which I assign the technical name "theorem". The term "theorem" has a precise definition in mathematical logic, say, "the element of a recursive set of well-formed formulas closed under logical consequence" where "logical consequence" has a precise definition in terms of the smallest relation satisfying various purely syntactic constraints. However, I also have the informal term "theorem" and "logical consequence" from the usual mathematical vernacular. These don't have formal definitions. A theorem is roughly just something interesting that we've proved about some mathematical objects. But in mathematical logic, the objects may be those that I've clumsily called "theorems". So to avoid the inevitable confusion, I start distinguishing the informal theorems as "metatheorems" and the mathematical objects as "object theorems", and I go on to say that all my prose exposition is the "metalevel", while the formal mathematical objects are the "object level." As I say, this distinction is formally clarified once you start formalising your "metalevel", at which point, the term "metalevel" takes on a technical role, rather than merely clarifying the ambiguity arising from our choices for technical terms. Edited by Phil Scott on Aug 10, 2011 - 7:01 AM |

•MoeBlee
aka I. Kabruob Usergroup: Members Joined: May 19, 2005 Total Topics: 10 Total Posts: 352 |
Posted Aug 10, 2011 - 11:15 AM:
Spoonwood wrote: What specific remark(s) by me do you think incorrect or unreasonable?I don't agree with MoeBlee Edited by MoeBlee on Aug 10, 2011 - 11:24 AM |

This thread is closed, so you cannot post a reply.