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

[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"?

[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.

[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)