FOM: 70:Efficient Formulas and Schemes

[Stephen Fenner]

On Tue, 2 Nov 1999, Raatikainen Panu A K wrote:

> FACT. The property of being efficient is not decidable; in fact, it 
> is not even r.e. It is co-r.e.
> 
> Take some simple contradiction, say  P(a) & -P(a), with complexity 
> 6 . If one manages to demostrate that a sentence/theory more 
> complex than this is efficient, one has also demonstrated that the 
> sentence or theory is consistent (for if it is inconsistent, it is 
> logically equivalent to a shorter formula P(a) & -P(a), and therefore 
> not efficient). But the set of consistent sentences is not r.e., and 
> consequently the set of efficient sentences and theories is not r.e. 

You show that the beta-efficient sentences/theories form a subset of the
consistent ones, but this doesn't imply that the former is noncomputable
(or non-r.e.) simply because the latter is.  Nevertheless, you're right
that the set is co-r.e., and it's a reasonable guess that that it's 
non-r.e. as well.

This set (of beta-efficient sentences/theories), which I'll call bE, seems
to be closely related to the set R of Kolmogorov random strings.  R is
co-r.e. and Turing-equivalent to the halting problem.  It also bears some
resemblance to the set MIN of minimal programs:

MIN = { e | the partial function computed by the e'th Turing machine is
            different from that of the i'th machine, for all i < e }.

A lot is known about MIN.  In particular, it is Turing-equivalent to 0''
(the halting problem relative to the halting problem).

CONJECTURE: bE is recursively isomorphic to (a different coding of) bE.

Steve