FOM: the relevance of relevance for complexity calibration

[Neil Tennant]

Harvey Friedman writes [and I supply some useful defined symbols]:
__________________________________ 

The problem with such proposals [as Tennant's] is the following. It
likely grossly overstates the complexity of sentences. Consider the
statement [S]: "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 [S*] 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 [of S] with a complicated Pi-1-4 sentence [P]. However,
this equivalence [of S with P] is no more likely to meet criteria such
as the one you are proposing than, say the known equivalence of [T]:
"every uncountable ANALYTIC set of reals contains a perfect subset"
with (for all x in V(omega))(x = x). over ZFC.
__________________________________

I take it that the complexity criterion that I was proposing would
have to vindicate the assignment to S of the complexity Pi-1-4,
i.e. that of P.  This means that there would have to be a proof in CR
[Classical relevant logic] of P from S (plus axioms of ZFC) and a
proof in CR of S from P (plus axioms of ZFC). The two proofs would
bring out the required intimate connection between the original
mathematical claim S and its complexity calibrator P. My untutored
intuition is that if "[b]y nontrivial analysis of the set theory
involved, one proves the equivalence [of S] with...[the] Pi-1-4
sentence [P]", then the two proofs (left to right and right to left)
ought to be relevantizable, and hence yield proofs in CR (after
cut- and dilution-eliminations) *with the needed premisses still being
used in the resulting relevant proofs*.

By contrast with this, take the situation where the sentence T is
"equivalent" to (x)(x=x) modulo ZFC only because T is a theorem of
ZFC. Its theoremhood seems to inflict a strange collapse of genuine,
intrinsic complexity. My suggestion was that the fault might lie in
the use of standard, irrelevant logic. The claimed "equivalence" of T
with (x)(x=x) modulo ZFC embodies an irrelevance. Again, my untutored
intuition is that, while there could well be a CR-proof of T from
(x)(x=x) modulo ZFC, it is unlikely that there would be a CR-proof of
(x)(x=x) FROM T modulo ZFC---where I emphasize the word FROM in order
to stress the likelihood that in the cut-elimination and
dilution-elimination process we would cut down to the empty set of
premisses, so that (x)(x=x) wouldn't be proved (in CR) FROM any
substantive premisses at all. It would be revealed, rather, as a
logical truth, following from the empty set of premisses, rather than
'from' T plus various axioms of ZFC.

If this is right, then the CR-proof-based complexity criterion I was
suggesting might have done some work. But I do confess in response to
Harvey's scepticism that I haven't the foggiest notion how to set
about proving that no CR-proof of a conclusion like (x)(x=x) would
involve non-trivial, genuine and relevant USE of premisses. I hope,
though, that this has clarified how I imagined the proposed criterion
would work out on these cases. It seemed to make good a priori sense,
hence worth venturing as a proposal.

Neil Tennant