Saturday, February 02, 2008

Metalanguages

This post probably just indicates that I am missing some key bits of knowledge. Why are all metalanguage classical (at least the ones I've seen)? Are there not any non-classical ones? Are there reasons for not using a non-classical metalanguage or there not being any, apart from making things more complicated? Surely there are discussions of these things somewhere...

On a different note, googling {{"non-classical metalanguage"}} yields 5 results. After this post it will probably yield 6.

9 comments:

Justin said...

I got five, one of which is your post. Perhaps there is a law of conservation of pages with "non-classical metalanguage" included.

Shawn said...

Ah. I got 4 hits without repeats before I posted. With repeats it came to 5. That was the number I was using. I wasn't sure which would be better really.

Kenny said...

I think there's a few people that do intuitionist meta-theory - but I remember the first time I took a class on intuitionist logic, we used a classical meta-theory, which really annoyed me at the time. Now I can understand why both would be interesting.

But I think the explanation is just that more people are interested in non-classical logic than there are people who actually believe that classical logic isn't the right one. And as long as classical logic is the right one, you'll be doing the meta-theory that way, even when studying interesting non-classical logics.

Greg said...

Historical note: In Carnap's Logical Syntax, the metalanguage he uses to analyze Language I is non-classical -- it's Language I itself. (Carnap took this to be a clear refutation of the Tractarian view that you cannot meaningfully talk about a language within that same language.)

Shawn said...

Kenny,
That sounds like a good explanation of it. Although, it seems like it would at least philosophically interesting to see what sort of metatheory you get by using, say, intuitionistic logic. Especially since contraposition sees so much action.

Greg,
Good point. Do you happen to know in what ways Language 1 is non-classical?

When I read that bit in Logical Syntax I felt like Carnap was not giving a reasonable interpretation to TLP, but I don't have a more reasonable one to give on that point. It has been, at best, obscure to me why TLP Wittgenstein says that you can't talk about syntax in a language. There are times when I feel like I have some grip on it, then I stop having that feeling. He generally doesn't like the idea of metalanguages in TLP, but I don't know what was being said about metalnaguages at that time (or now really) to motivate and explain them. That whole transition is somewhat opaque to me, from no metalanguages to metalanguages.

Noam said...

One example of a non-classical metalanguage is Martin-Löf's type theory (ML). You can read a mini-description
here. It might seem like working in a constructive metalanguage like ML is a handicap (like Kenny suggests), because any proposition P must be given a constructive proof. However, this has the important consequence that when reasoning from P, we can reason by induction over the canonical proofs of P, which is much harder to do in classical metalanguages.

I think a very good discussion of classical vs non-classical metalanguages (or "realist vs anti-realist positions") is Dummett's Logical Basis of Metaphysics. One of the questions he asks is whether the logical laws can be "justified", and draws the conclusion that this is possible for intuitionistic logic, but much harder for classical logic. Essentially, his argument exploits the property that in intuitionistic logic, it is possible to reason about canonical proofs.

Shawn said...

Kenny,
I just realized that you seemed to say that choice of metalanguage expresses a belief in what logic is "the right one". Is that what you meant? It hadn't occurred to me that choice of metalanguage would be so philosophically important, although thinking about metalanguages is new to me. Do you know of anyone that discusses that idea?

Justin said...

Shawn, I think that idea is explicitly up for grabs in the Gödel-Carnap debate (with Ricketts and Goldfarb doing Carnap's defense, of course).

Greg said...

Language I in Carnap's LSL has (objectual) variables, but lacks quantifiers. Generality is expressed by unbound variables, like in a middle school algebra book; i.e., what we would today write as 'For all x, y (x+y=y=x)', lng.I just has 'x+y=y+x.' The result is that existential quantifier can't be defined.

I heard (I think from Jeremy Avigad) that Language I is either identical or nearly identical to primitive recursive arithmetic.