FOM: complexity of sentences

[Harvey Friedman]

Tennant writes 12:23PM 4/21/98:

>This other sense of "relevant" that I think *will* work is given by
>the notion of a cut-free, dilution-free proof in a sequent system with
>appropriate logical rules for introducing logical operators on the
>left and/or on the right of a sequent. For such a system (call it CR)
>we have the following metatheorem:
>
>        If there is an ordinary classical proof of the sequent X:Q
>        then there is proof in CR of Y:Q or of Y:emptyset, for some
>        subset Y of X.
>
>Note that I am not claiming that proofs in CR will be as economical as
>ordinary proofs using cuts. We do know, however, that cuts can be
>eliminated (Gentzen's Hauptsatz); and then a linear transformation
>will turn the resulting cut-free proof into a cut-free, dilution-free
>proof, in CR, of some subsequent of the original result. Only if a
>premiss survives this process can it said to be relevant to the
>conclusion of the sequent.
>
>Thus my proposal for "complexity calibration" of any theorem T will be
>that for the complexity-diagnostic sentence C there should be proofs
>in CR of two sequents of the form
>
>        X,T:C   and     Y,C:T
>
>where X and Y are subsets of the set of axioms of ZFC. In the first
>proof (of the sequent X,T:C) the premiss T will "really be doing some
>work, modulo X" to yield the conclusion C. Likewise, in the second
>proof (of the sequent Y,C:T), the premiss C will "really be doing some
>work, modulo Y" to yield the conclusion T.

The problem with such proposals is the following. It likely grossly
overstates the complexity of sentences. Consider the statement "every
uncountable co-analytic set of reals contains a perfect subset." I had said
earlier that this was in complexity class Pi-1-4 and no better over ZFC.
Yet if we formalize this sentence in the standard way in ZFC, then we get a
sentence that is of horrifically large complexity as written. I.e., recall
that we have to define real numbers, sigma algebras of sets of reals, Borel
sets, analytic sets as projections of Borel sets, perfect sets, etcetera.
By nontrivial analysis of the set theory involved, one proves the
equivalence with a complicated Pi-1-4 sentence. However, this equivalence
is no more likely to meet criteria such as the one you are proposing than,
say the known equivalence of "every uncountable ANALYTIC set of reals
contains a perfect subset" with (for all x in V(omega))(x = x). over ZFC.

Here is a modification of your proposal, not involving relevant logic, that
is subject to the same objections. One asks that the statement under
investigation and its "proposed simpler logical form" be provably
equivalent in predicate calculus. This would also presumably assign very
large complexities to sentences over ZFC.

I think this matter can be clarified further by examining * = "every
uncountable analytic set of reals contains a perfect subset." There are two
"direct formalizations" of this. First there is the at least fourth order
formalization involving sets of reals, sigma algebras of sets of reals,
etcetera. Then there is the formalization within the language of second
order arithmetic using standard appropriate treatment of analytic sets of
reals, which comes out to be pi-1-4. Then there is the least complexity of
a sentence which is provably equivalent to * within RCA_0. This turns out
to be pi-1-2. So note the three different complexity measures.

Here is a relevant conjecture. Call a sentence of predicate calculus
logically tight if and only if it is not logically equivalent to any
sentence of lower complexity. The conjecture is that sentences occurring in
actual mathematics are (generally) logically tight. This conjecture can be
interpreted in two different ways. Firstly, without unraveling
abbreviations. This seems like a safe bet since mathematical statements
seem to always be quite short. Once they threaten to get long, one brings
in abbreviations. Secondly, with unraveling abbreviations. Then the
conjecture seems much more problematic and needs systematic investigation.
NOTE: there is a standard inductive definition of the complexity of
formulas in predicate calculus by induction on the formulas. The complexity
classes that are inductively defined are Sigma_n,  Pi_n, and Boolean
combinations of Sigma_n.