# Metalogicians! A question for you! **URL:** \ **Category:** Factual Questions\ **Created:** [May 10, 2015, 3:32am UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677 "2015-05-10T03:32:13Z")\ **Posts on this page:** 11\ **Page:** 1
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 10, 2015, 3:32am UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/1 "2015-05-10T03:32:13Z")
I would have affirmed the following two statements, though not very confidently, if I’d been asked: 1. If N is a proof of a statement about objects in a domain D, then N is a derivation in a language interpreted as referring to D 2. Every semantic rule about a language L, as expressed in a metalanguage L-prime (i.e. every rule in L-prime concerning what symbols in L refer to what objects in L’s domain) can be effectively considered as a syntactic rule in a meta-metalanguage L-prime-prime (i.e. as a rule concerning which symbols in L-prime may appear in what order in to satisfy requirements of well-formedness and valid derivation). For each of these two claims, can you tell me whether they are A. Trivially true B. True but not trivial C. Controversial D. False but some serious people argue true E. Trivially false? Or something else? (For example, nonsense or at least needing clarification) ---
**Author:** ![Hari\_Seldon](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/hari_seldon/32/5173_2.png) [@Hari\_Seldon](https://boards.straightdope.com/u/Hari_Seldon)\ **Post date:** [May 10, 2015, 1:20pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/2 "2015-05-10T13:20:44Z")
You have just illustrated why I have little interest in logic. They seem true, but seem so ultra-pendantic that I have no idea what their formal status is. ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 10, 2015, 1:31pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/3 "2015-05-10T13:31:15Z")
> [@Hari\_Seldon](#): > > You have just illustrated why I have little interest in logic. They seem true, but seem so ultra-pendantic that I have no idea what their formal status is. Oh please don’t let this kind of thing turn you off of logic. They are _totally_ pedantic. It’s just that someone said I was crazy for holding them (well, natural english versions of them) and was sort of pulling rank on me credential wise.\* I was surprised, and am trying to get other opinions to see if I was as crazy as this person seemed to imply. \*Yet they don’t have any clear expertise, it’s just that they “teach metalogic.” Well, frankly, I could probably teach metalogic too given a week or two of notice, but I have no way to prove that so I was “helpless”… ---
**Author:** ![Hari\_Seldon](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/hari_seldon/32/5173_2.png) [@Hari\_Seldon](https://boards.straightdope.com/u/Hari_Seldon)\ **Post date:** [May 10, 2015, 11:47pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/4 "2015-05-10T23:47:00Z")
I have even taught courses in logic and set theory, but I didn’t enjoy them. But metalogic is too meta for me. ---
**Author:** ![TATG](https://avatars.discourse-cdn.com/v4/letter/t/50afbb/32.png) [@TATG](https://boards.straightdope.com/u/TATG)\ **Post date:** [May 11, 2015, 3:52am UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/5 "2015-05-11T03:52:45Z")
I’m not sure how to interpret 1. I’d normally think that proofs are seperate from interpretations. If I had a proof of A I’d think that is a proof that holds for any interpretation of the language. So false, with the caveat that I might not understand what you mean by 1. 2 seems non-sensical. L’ is just a function from constants to objects in a domain. It isn’t a logic (or meta-logic), and has no rules of well formedness or derivation. > [@Frylock](#): > > It’s just that someone said I was crazy for holding them (well, natural english versions of them) and was sort of pulling rank on me credential wise. But they didn’t say why they thought you were wrong? ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 11, 2015, 12:03pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/6 "2015-05-11T12:03:29Z")
> [@TATG](#): > > I’m not sure how to interpret 1. I’d normally think that proofs are seperate from interpretations. If I had a proof of A I’d think that is a proof that holds for any interpretation of the language. So false, with the caveat that I might not understand what you mean by 1. I think what you’re calling a proof is what I meant by "derivation.’ I understand a derivation to ne just a series of sequences validly derived (natch) from each other. It’s supposed to be a purely syntactic idea. Meanwhile I understand a proof to be something that establishes that something is true. I.e. it’s a semantic idea. The discussion I was in started when someone said they had their propositional logic students “derive” the law of explosion. Someone else chimed in and said, in so many words, that you can’t “derive” the law of explosion, it’s the kind of thing that gets “proved.” I went and stuck my big mouth into the situation by suggesting that a “proof” of the law of explosion is _also_ a “derivation” since (as per the claim in the OP) every proof is just an interpreted derivation. If, in a meta-logic, you “prove” that explosion holds in the relevant logic, then what you will have done is _derive_ a sequence in the metalogic which, on interpretation, states “the law of explosion holds in the logic.” > [@](#): > > 2 seems non-sensical. L’ is just a function from constants to objects in a domain. What I said in 2 wasn’t meant to characterize the entirety of L’, rather, it just mentioned a particular relevant fact about L’. I meant it to be assumed L’ has all the well-formedness and derivation rules etc, but didn’t think it necessary to actually spell them out since, well, L itself isn’t spelled out. Here’s something I offered in clarification in another context: > [@](#): > > As to an example, here’s what I have in mind. > > Say you’ve got a language L which contains the name c. And in L-prime, you can express the following true\* statement: “in L, c refers to Carol.” > > Given that, I’m thinking, we could then create an L-prime-prime via which we can express the following statement: “In L-prime, ‘c refers to Carol’ is well formed, and ‘c refers to Cassandra’ is not.” (Remember, in L-prime-prime, “Carol” and “Cassandra” are considered as empty strings, not as referents to Carol and Cassandra.) > > If we were to create such an L-prime-prime, I’m thinking, the things L-prime-prime says are well-formed in L-prime will be the same things that L-prime says are true of L. > > Something like that. > > \*True by stipulation, as I’m imagining a case in which we’re using L-prime to define L. > [@TATG](#): > > But they didn’t say why they thought you were wrong? Not really. Just counterasserted. She was, unfortunately, just kind of ticked off that I’d contradicted her, so she kind of just said “No you’re wrong. I teach metalogic.” and left. ETA: I just deleted a comment about Goedel because I remembered Goedel came up in a discussion with the same person, but not on this topic. ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 11, 2015, 1:17pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/7 "2015-05-11T13:17:19Z")
Here’s something I wrote elsewhere, in response to someone else’s requests for clarification, which may help here. > [@](#): > > First can I ask, IS there a distinction between proof and derivation? If so, what is it? The two claims I laid out came out of a discussion I’d had with someone I was assuming would know what they’re talking about, who drew a very sharp distinction between proof and derivation–a distinction they took to be quite crucial in any discussion that might use either of the terms–and if I understood them correctly, they were assuming that proofs have a semantic character, being proofs that something is true of a domain, while derivations are merely syntactic, being just correctly shuffled symbols. This distinction seemed okay by me based on my vague memories from my own logic courses and some subsequent reading, so I took it on board in formulating my two claims. But is that not the usual distinction? > > The overall issue I’m wrestling with is this. I’ve always had the idea, not really explored much, that while there is a real distinction between syntax and semantics, nevertheless semantics effectively supervenes on syntax. That, in other words, you get semantics when you have the right system in front of you considered purely syntactically. True or not, I have always thought this is at least a reasonable idea. Is it not? > > The causal explanation for my having this idea (not a rational justification, a causal explanation) is my adolescent reading of Hoffstedter’s Goedel Escher Bach, in which he argues (I’ve just double checked in the preface of the 1999 edition) that what a semantic system is is a syntactic system with the right kind of pattern in it. That’s an idea that infected me at a tender age and if it should have been beat out of me during my graduate education, that never happened! > > I think if I can get clear about what I just asked about above, that will help me out with what I was trying to get at with the two claims I opened up this exchange with. But to try to clear confusion on #2, put more naturally (because I clearly failed when trying to be more technical!) the idea is supposed to be this. If you can, in one language, show that a set of statements are true in a domain, using a set of proofs (P), then you can, in another language, (where that other language takes the first language as its domain), define a validity predicate which applies to strings in the original language, such that all and only the elements P are valid–AND the validity predicate in the second language (and indeed, the second language itself) need make no reference at all to the domain of the original language. (Albeit they will make reference to symbols which themselves, in the original language, refer to elements in the domain. But referring to symbols which refer to things is not the same as referring to the things themselves. Use/mention etc.) > > Importantly, this should be understood as a claim only about FORMAL languages. > > Thank you for your patience. It’s been a long time since I tried to do logic. ---
**Author:** ![TATG](https://avatars.discourse-cdn.com/v4/letter/t/50afbb/32.png) [@TATG](https://boards.straightdope.com/u/TATG)\ **Post date:** [May 11, 2015, 3:47pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/8 "2015-05-11T15:47:46Z")
Some general comment about terminology (since this seems to be what a lot of your issue is about.) I would expect to see “proof” used in two main senses in logic texts. One would be defined, e.g. (something like) “X is a proof of A iff A is a sequence of wffs such that…”. The other would be the more natural language usage, so (something like) proofs of mathematical theorems by some mix of natural language and formalism. > [@Frylock](#): > > I think what you’re calling a proof is what I meant by "derivation.’ I understand a derivation to ne just a series of sequences validly derived (natch) from each other. It’s supposed to be a purely syntactic idea. Is this a purely formal notion? Is validity relative to a logic? > [@Frylock](#): > > Meanwhile I understand a proof to be something that establishes that something is true. I.e. it’s a semantic idea. I’m not sure what this means. Is a proof a formal notion? By semantic do you mean the sort of thing meant by the semantics of a logic? (And when you talk about domains, do you mean domains as per the semantics of First-Order Logic?) > [@Frylock](#): > > The discussion I was in started when someone said they had their propositional logic students “derive” the law of explosion. Someone else chimed in and said, in so many words, that you can’t “derive” the law of explosion, it’s the kind of thing that gets “proved.” This sounds like a more normal claim about a logic. Consider the following claim about propositional logic: for every wff A, (A v ¬A) is derivable from the empty set. This is true, but by using propositional logic, all you can do is derive (one by one) for each A, (A v ¬A). I.e. you cannot derive the quantified (for all wff A…). But that seems to be about the power of the logic in question, rather than proofs vs derivations. (It may be that there was just some misunderstanding at this point in the conversation, or it may not be.) > [@Frylock](#): > > I went and stuck my big mouth into the situation by suggesting that a “proof” of the law of explosion is _also_ a “derivation” since (as per the claim in the OP) every proof is just an interpreted derivation. This sounds more like a definition that a claim. I’m going to guess at what you have in mind. You have a logic, and you can derive things in un-interpreted languages. But, of course, you want to know if _Socrates_ is mortal (or whatever the case may be). So you interpret the language, and poof, you now have a proof about Socrates! If we accepted these definitions, it seems like all proofs are derivations (once we abstract away from the interpretation). But this seems like a distinction that would cause confusion if it wasn’t spelt out. > [@Frylock](#): > > If, in a meta-logic, you “prove” that explosion holds in the relevant logic, then what you will have done is _derive_ a sequence in the metalogic which, on interpretation, states “the law of explosion holds in the logic.” In the case of explosion (and other similar cases), what you will do in practice is write a bunch of natural language sentences (mixed in with some formalism) and claim that this ammounts to a proof. It won’t be formalised. It likely won’t follow, step by step, by some standardly found rules of a logic (i.e. you won’t be able to look up the rules of, say, First-Order Logic and justify each step by a rule). Would that count as a proof for you? ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 11, 2015, 4:16pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/9 "2015-05-11T16:16:52Z")
> [@TATG](#): > > Some general comment about terminology (since this seems to be what a lot of your issue is about.) Yeah, I think there was terminological confusion. See below. > [@](#): > > > [@](#): > > > > The discussion I was in started when someone said they had their propositional logic students “derive” the law of explosion. Someone else chimed in and said, in so many words, that you can’t “derive” the law of explosion, it’s the kind of thing that gets “proved.” > > This sounds like a more normal claim about a logic. Okay, if this sounds like a more normal claim, then what is the distinction between derivation and proof that’s being assumed by someone who makes this claim? > [@](#): > > Consider the following claim about propositional logic: for every wff A, (A v ¬A) is derivable from the empty set. This is true, but by using propositional logic, all you can do is derive (one by one) for each A, (A v ¬A). I.e. you cannot derive the quantified (for all wff A…). This is exactly what I took her to be talking about. When she put it in terms of what can be “derived” and what can be “proved,” though, the sense I could make out of that was that she was calling symbol-shuffling within a language “derivation” and symbol-shuffling within a meta-language ABOUT that first language “proof.” > [@](#): > > But that seems to be about the power of the logic in question, rather than proofs vs derivations. (It may be that there was just some misunderstanding at this point in the conversation, or it may not be.) I don’t know, I’d have to ask her, I guess, what exactly she meant by “proof” and “deriviation” but that ship has sailed for various reasons. Conversation’s over. > [@](#): > > This sounds more like a definition that a claim. While I didn’t intend “every proof is an interpreted derivation” to be a definition (for example, you could have interpreted derivations that aren’t proofs!) I did take it to basically fall out trivially from what I took to be her definitions of “proof” and “derivation.” > [@](#): > > I’m going to guess at what you have in mind. You have a logic, and you can derive things in un-interpreted languages. But, of course, you want to know if _Socrates_ is mortal (or whatever the case may be). So you interpret the language, and poof, you now have a proof about Socrates! > > > [@](#): > > > > Exactly > > If we accepted these definitions, it seems like all proofs are derivations (once we abstract away from the interpretation). But this seems like a distinction that would cause confusion if it wasn’t spelt out. I’m getting that picture. Like I say, at the time I thought I was using _her_ concepts to communicate with her, and I was assuming her concepts were the generally accepted ones. But there are very open possibilities that, for one, I may have misunderstood her (thought it’s hard to see what she meant by ‘you can prove the law of explosion but not derive it’ if so), and for another thing, even if I understood her correctly she may have been using the terms in a way that is not typical. > [@](#): > > In the case of explosion (and other similar cases), what you will do in practice is write a bunch of natural language sentences (mixed in with some formalism) and claim that this ammounts to a proof. It won’t be formalised. It likely won’t follow, step by step, by some standardly found rules of a logic (i.e. you won’t be able to look up the rules of, say, First-Order Logic and justify each step by a rule). Would that count as a proof for you? Right, this came up in the conversation. She started talking about natural English proofs. In fact toward the end I began to suspect she may think proofs _only_ occur in natural English! (That’s definitely unusual, though, isn’t it?) I said in that conversation, intending it to be kind of a cheeky comment, not too serious, but I _did_ say it, “I hesitate to call those proofs.” Why would I say that? Because it seems to me that these natural-English proofs\* rest, intentionally or not, on an underlying formalism, in the sense that if you started asking why _they’re_ supposed to work, what you’re going to end up elucidating is–a formalism. \*I forget what it’s called, but there’s this phenomenon of something that gets called something like “logical English” which, as far as I’ve ever been able to tell, really _is_ a formalism, it’s just that it uses English words, mixed in with logical and set-theoretic notations. Only a very few select English phrases get used, with explicitly defined meanings. I don’t take this to be “natural language.” ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [May 11, 2015, 4:33pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/10 "2015-05-11T16:33:08Z")
> [@Frylock](#): > > (for example, you could have interpreted derivations that aren’t proofs!) Oops, that’s wrong, based on something else I said earlier about what I was trying to mean by “derivation.” Consider it deleted! ---
**Author:** ![TATG](https://avatars.discourse-cdn.com/v4/letter/t/50afbb/32.png) [@TATG](https://boards.straightdope.com/u/TATG)\ **Post date:** [May 11, 2015, 6:53pm UTC](https://boards.straightdope.com/t/metalogicians-a-question-for-you/719677/11 "2015-05-11T18:53:09Z")
> [@Frylock](#): > > Okay, if this sounds like a more normal claim, then what is the distinction between derivation and proof that’s being assumed by someone who makes this claim? The distinction _in this case_ would be that the derivation goes on within propositional logic, but you need to go outside it to prove the stated fact. But note, the way I think of the normal claim is someone says “you can prove/derive/deduce excluded middle in propositional logic”, and a second says, “well that isn’t precise, because blah blah you can prove instances blah blah meta-language or whatever”. As I am thinking of the situation, the assumption made by the respondent is that _their intolucoter_ is using derived to mean “derived within propositional logic”. (Or to put it another way, the point isn’t meant to be a terminological one.) > [@Frylock](#): > > I’m getting that picture. Like I say, at the time I thought I was using _her_ concepts to communicate with her, and I was assuming her concepts were the generally accepted ones. But there are very open possibilities that, for one, I may have misunderstood her (thought it’s hard to see what she meant by ‘you can prove the law of explosion but not derive it’ if so), and for another thing, even if I understood her correctly she may have been using the terms in a way that is not typical. To use “derive” to mean “using the inference rules of the logic” or some variant thereof is natural. I’d guess someone has at some point _made_ some clear distinction where “derivation” meant x, and “proof” meant y (in _some_ paper/course/textbook). But words are meant in many ways, doubley so in logic. The standard (or at least the ideal) would be to say which way one meant. > [@Frylock](#): > > In fact toward the end I began to suspect she may think proofs _only_ occur in natural English! (That’s definitely unusual, though, isn’t it?) That would be unusual unless one had an unusual definition of natural language.