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

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?