FOM: administrative note; the 'right' proof

[Stephen G Simpson]

Administrative note:

I will be away from e-mail for about 10 days starting immediately.  So
FOM will be silent.  However, FOM will resume around July 20.

AndrEs Eduardo Caicedo 25 May 1998 20:24:48 writes:

 > Is there any *formal* way of, given a proof, detect its relevance? 
 ...
 > A possible approximation to a formalization of the problem can be:
 > 
 > "If a provable assertion has complexity G -where G=\Delta^0_n, or
 > \Sigma^1_1, etc-, then there is a proof of it containing only assertions
 > of complexity F_G", were F is definable in some way. This perhaps is
 > false, perhaps for obvious reasons, but I don't know. If it is true, we
 > are trying to measure relevance here by bounding the complexity of the
 > statements of the proof in terms of the complexity of the problem, so the
 > proof is 'close' in some sense to the problem. But perhaps there are more
 > accurate measures of relevance.
 > 
 > Any thoughts?

The following thought occurs to me.  A necessary condition for a proof
P of a theorem T to be "relevant" is that P should be formalizable in
S_T, where S_T is the weakest natural formal system in which T is
provable.  Since determination of S_T for given T is the concern of
reverse mathematics, we could refer to this kind of relevance as
RM-relevance.

In the example that you gave, T = "there exist incomparable Turing
degrees", the proof by Cohen forcing over a transitive model of ZFC is
not RM-relevant as it stands, because the existence of transitive
models of ZFC is an unnecessarily strong assumption.  But perhaps this
proof can be converted to a proof that is RM-relevant, e.g. by Cohen
forcing over the standard model of arithmetic.

In other cases, RM-relevance may be interesting but not exactly what
you were looking for.  As an example, let T = the local existence
theorem for solutions of the differential equation dy/dx=f(x,y),
y(0)=0, f continuous in some neighborhood of (0,0).  In this case,
reverse mathematics has revealed that S_T = WKL_0.  But the standard
textbook proof of T via the Ascoli lemma is clearly not RM-relevant,
i.e. not formalizable in WKL_0, because the Ascoli lemma is not
provable in WKL_0.  And the proof in WKL_0 is longer and trickier than
the standard proof.  See
http://www.math.psu.edu/simpson/papers/hilbert/.

Is this something like what you were looking for?

-- Steve

Name: Stephen G. Simpson
Position: Professor of Mathematics
Institution: Penn State University
Research interest: foundations of mathematics
More information: www.math.psu.edu/simpson/