[FOM] syntactic power/3

[Jacques Carette]

That is not truly robust either -- at the very least, you ought to have 
" let t = t' in t'' " as a language former. In all sorts of places, 
including counter-examples to Richardson's uniformity conjecture are due 
to 'sharing' not being accounted for properly. This is also well-known 
in computer science in general, where loss of sharing causes quite 
unnecessary exponential blow-up; in mathematical practice, one always 
gives names to intermediate results, without ever really thinking about 
it. This has very strong complexity implications.

Eventually, if you want robustness meta-theorems, you'll likely want to 
use ideas from Kolmogorov Complexity and/or Minimum Description Length.  
I guess it depends on whether the sizes you end up encountering are 
small [ <1000 in your current definitions] or quite large [ > 50,000 is 
likely enough].  What we know from Chaitin's number Omega and Busy 
Beaver (and so on) unfortunately might imply quite small sizes [ < 100 
], which makes all counts, even ones based on KC, extremely fragile. At 
those size, extremely small changes in vocabulary can change the results.

For a concrete example, in number theory the cyclotomic polynomials (and 
roots of unity, best represented via cyclotomic polynomials) grow 
exponentially fast in representation size [eventually!] and are a 
frequent source of counter-examples to naive complexity results - 
especially for factoring, for example. But there are 'vocabularies' in 
which one can represent cyclotomic polymials without the exponential 
blowup. There are conjectures that cyclotomics are the only 
'obstruction', and so this change of vocabulary would be enough to avoid 
blowup.

If this is of interest, I can provide references (some of which will be 
to my own work).

Jacques

PS: I find the questions quite interesting. It would be fascinating if 
for some of the pairs of theories, the best answer would be "they are 
the same", not because numerically the lengths involved are equal, but 
that the ordering depends in a fundamental way in the method of counting.

On 2019-10-13 3:07 p.m., Harvey Friedman wrote:
> Regarding https://cs.nyu.edu/pipermail/fom/2019-October/021728.html
>
> For robustness I think it is better to count the number of distinct
> atomic formulas x = y, x epsilon y, that appear.
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom