FOM: administrative note; the 'right' proof
Stephen G Simpson
simpson at math.psu.edu
Thu Jul 9 15:47:09 EDT 1998
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/
More information about the FOM
mailing list