# [FOM] Classical/Constructive Arithmetic

Andrej Bauer Andrej.Bauer at andrej.com
Mon Mar 20 12:13:02 EST 2006

```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
```