[FOM] 576: Game Correction/Simplicity Theory 1

[Harvey Friedman]

Hendrik Boom wrote:

> I was playing with the complexity of definition of specific integers
> some decades ago.  I used more or less the same definition for
> complexity you did, but I used Church lambda expressions instead of the
> your relational notation.  Because you use existential quantifiers
> you'll have the sema potential difficulty I did.  Quantifiers can be
> nested deeply, leading to more and more different bound variables.  It
> becommes possible to pack a *large* amount of into a variable.  Then
> each use of a variable can contribute a large amount of information
> (and intuitive complexity) to the definition.
>
> I decided to measure complexity of variables by the logarithm of the
> number of variables there were to choose from.  Perhaps requiring
> variables to be words made of letters in a fixed alphabet is a more
> intuitive (and computationally simpler) to accomplish the same objective.

Measuring complexity of integers is, I think, a quite different
project than measuring the complexity of fundamental mathematical
notions as in Simplicity Theory.

One major difference that I see is that the complexity measures of the
fundamental notions are going to be quite small integers, as the usual
definitions are fairly small, related to the fact that they are
fundamental notions. Also existential quantifiers can be banned in
certain natural circumstances, where one is looking only for the
complexity of purely universal definitions.

I wrote

> COMPLEXITY DEFINITION. Let M be a relational structure. We use and,
> or, not, if then, iff, formal, therexists, =, together with the
> relation, constant, and function symbols interpreted by M. The
> complexity of a formula in L(M) is the total number of relation,
> constant, and function symbols appearing in the formula.

I meant to include = among the items to be counted. I.e.,

COMPLEXITY DEFINIITON. Let M be a relational structure. We use and,
or, not, if then, iff, forall, therexists, =, together with the
relation, constant, and function symbols interpreted by M. The
complexity of a formula in L(M) is the total number of relation,
constant, and function symbols, and =, appearing in the formula.

Harvey Friedman