[FOM] Classical/Constructive Arithmetic

[Andrej Bauer]

On Saturday 18 March 2006 10:18, Harvey Friedman wrote:
> 4. Examples where the known proof is nonconstructive, and where one can
> give a constructive proof, but it is known that all constructive proofs are
> grotesque (e.g., extremely long, or extremely unpleasant, etc.).

A general strategy for finding such things is the following. Take a theorem X 
which holds classically but not constructively. Consider its constructive 
counterpart Y (which may or may not be a weakening of X), which usually has a 
reasonable proof. Now take a theorem Z which is a special case of X but is 
not covered by Y. If you pick Z well, a constructive proof of Z might be 
rather complicated. Example:

  Theorem X (Tietze's Extension Theorem for for metric spaces):
  Let S be a closed subset of a metric space M. Every locally uniformly
  continuous f:S-->R has a continuous extension f':M-->R.

  Theorem Y:
  Let S be a locally compact subset of a metric space M. Every locally 
  uniformly continuous f:S-->R has a locally uniformly continuous extension 
  f':M-->R.
  (See Bishop's "Constructive Analysis", Section 4.5 for details.)

Now to get a complicated Z, take something that follows trivially from X but 
does not conform to Y. In particular, we consider the complete separable 
metric space M = R^omega (a countable product of copies of the reals) with 
subspace S = Z^omega, where Z is the set of integers.

  Theorem Z:
  Every continuous map Z^omega-->R has a continuous extension to R^omega-->R.

I don't know of a general constructive theorem from which Z would follow. 
However, Z is valid constructively and the shortest proof I know is too 
horrible for me to try to read it again.

Andrej