expressivity

[gusl]

hmm... proof theory... (imagine a lip-licking emoticon, or a Homer Simpson voice)

from Around Gödel's Theorem - Ch 6.4: On the size of proofs

...
Theorem on the Size of Proofs.If T is a fundamental formal theory, and a closed formula H is not provable in T, then for each computable function f(x), which grows to infinity, there is a theorem K of T such that

|K|_T+H < f(|K|_T). [ |K|_T+H means "the size of the proof of K in theory T+H" ]

For example, let use take f(x) = x/100. There is a theorem K1 of the theory T such that its proof in the extended theory T+H is at least 100 times shorter than its shortest proof in T. You can take also f(x) = x/1000, or sqrt(x), or log10(x) etc.
...

I wonder if this is relevant to the broader concept of expressibility.

Obviously there can't be a (shortest proof <~> shortest program)-analogous result: since all good languages are Turing-equivalent, then for all problems, its Kolmogorov Complexities are bounded by a constant of each other (the size of the interpreter for the language into a standard computing machine).

When thinking of Logic and Computation side by side, I always think of this difference: logics have limited expressivity, whereas computational systems always have maximum expressivity.

So when we talk about "expressivity" in the context of programming languages, we mean something else entirely: how easy and natural is it to express what we want? Maybe we should use a new word, like "expressibility".

The literature on this subject seems to be very poor: Felleisen being the only reference I could find, besides fare of course. I think this warrants a philosophical essay at the very least, in order to properly define "expressivity/expressibility" and discuss possible measures.

Comments

[mathemajician.livejournal.com]

You might also be interested in one of my papers "Solving Problems with Finite Test Sets" which you can find at www.vetta.org/papers.html

[gustavolacerda.livejournal.com]

That's lovely! It's exactly the kind of "fundamental constraints" result that I find so nice... which is probably the main reason I like KC in the first place.

[gustavolacerda.livejournal.com]

was this your own idea?

This "fundamental constraint" idea is also the reason I got interested in Chaitin, although I've become skeptical of him.

What do you think of van Lambalgen's critique of Chaitin? How far do you believe Chaitin yourself?

What do you think of "a 10-pound theory can never prove a 20-pound theorem"?

uncomputability of BB(n)

[gustavolacerda.livejournal.com]

Is there a computable upper bound to the busy beaver function?
Maybe you can prove that there can't be one by a similar argument (maybe the same argument!).

The speed prior "solves" uncomputability by going around it. Maybe you could use a similar construction to prove that those possible exceptions to the theorem are not worth waiting for / worrying about. So, as an empirical mathematician, you conclude that they are true until. And if you don't like non-monotonicity, we can always have a mathematics with Bayesian belief revision instead.

I know that there exists probabilistic number theory, but I don't know about other areas of mathematics.

[mathemajician.livejournal.com]

Yeah, KC things are cute. The problem is that every time you're doing something and you think that you have a result that looks really interesting you naturally start to think it could be useful for something... and then you remember how horribly impossible it is to compute or even estimate.

[mathemajician.livejournal.com]

Yes it was my idea. It came to me while I was reading about KC and Goedel incompleteness in Li and Vitanyi's book about ten years ago.

At the time I was thinking about whether a 10 pound *theorem* could require a 20 pound proof. My conclusion was that at least a 10 pound theorem couldn't fail with a 20 pound counter example. That's how I had the idea for the paper.

I haven't read van Lambalgen before.

Re: uncomputability of BB(n)

[mathemajician.livejournal.com]

There is no computable upper bound to the busy beaver function. It's perhaps the most important property of the function.

I'm not sure if mathematics would work if you had things that were only true up to the limits of practical computation. I suspect that mathematics would start to badly fall apart?

[mathemajician.livejournal.com]

By the way. I wrote a very basic paper about intelligence and complexity recently. It's not published so I don't want it circulated just yet, but perhaps you'd like to read my draft?

[gustavolacerda.livejournal.com]

sure thing.

[gustavolacerda.livejournal.com]

I haven't read van Lambalgen before.

He seems to make a convincing case that many of Chaitin's claims aren't as remarkable as they seem, and that most of his philosophical conclusions are totally unwarranted.

I'd like to hear someone else's opinion. Maybe someone at IDSIA would have written something about this debate? (van Lambalgen's criticism was censored in unusual circumstances, which seemed politically motivated, so I'm not sure if his criticisms are very well known)