I would have affirmed the following two statements, though not very confidently, if I’d been asked:
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
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)
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”…
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.
But they didn’t say why they thought you were wrong?
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.”
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:
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.
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.
Is this a purely formal notion? Is validity relative to a logic?
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?)
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.)
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.
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?
Yeah, I think there was terminological confusion. See below.
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?
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.”
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.
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 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.
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.”
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.)
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.
That would be unusual unless one had an unusual definition of natural language.