Dear Bruno:
These are some of the things I want to explore as a result of formulating
my question re the UD.

##
Advertising

To start:
1) Are you saying that the UD contains all other computations as data?
2) By your comment "You confuse computability and provability." I think you
mean the UD indeed contains all computations as data. But for sake of
covering all bases I thought "compute" = "prove" was established by
Turing. Though I know some want to expand beyond this. Regardless, IMO
even if it has all this data it is still an expression plus data plus
self-delimiter that outputs [proves] a value. That is the "sense" I am using.
3) If in order to work the UD contains all other computations as data then
the UD is a highly complex program. A small expression with a lot of data
and a very large self-delimiter. If you have to put the data string in to
get it out that is a sign you are working with a random string. Random
strings are complex and I thought "all Theorems" was a very low complexity
object. Or is it random?
4) Why not run a highly parallel computer rather than a UD? [That is rather
like a part of my model.]
5) My meaning for "knowing" is at first order like proving. Chaitin is
actually talking about the complexity of the FAS's theorem checker as the
complexity of the FAS. The theorem checker "knows" all theorems of the
FAS. If a proof is an elegant proof by default then the theorem checker
also knows this proof or it would not know how to check the output for
theorem hood. It can prove this proof is elegant because there is no other
choice.
Hal