[FOM] (no subject)

[Jeremy Clark]

Dear FOM subscribers,

I would like to offer for consideration an interpretation of constructive
analysis as described in Bishop and Bridges' book. I think it is a clean
way to bring constructive analysis down to a completely 'finitistic' level.
I would greatly appreciate any comments on this system and how I
might develop it into a more substantial piece of research. What follows
assumes of the reader some understanding of the nature of constructive
analysis.

We shall use the syntax of second-order logic of arithmetic: variables
x,y,z,... denote  natural numbers, X,Y,Z denote functions mapping
|N to |N. functions written as A(x,...,X,...) denote primitive recursive
functionals.

We define *simple* properties of second-order objects to be those
of the form (x)A(x,X). So, for example, being a real number is a simple
property. For two reals to be equal is a simple property. There
are many others.

The general form for a theorem in constructive analysis is this:

(1)          (X) [ (x)A(x,X)  =>  (y)B(y,X) ]

The simplest possible example which isn't completely trivial is that
the relation of equality defined on the reals is transitive. One can
check that it is of form (1) quite easily.

My suggested replacement for this form is the following: a construction
\gamma is given, which satisfies:

(2)          (X) (y) [ B(y,X) V ¬A(\gamma(y,X), X) ]

The intuitive idea is that if we have a counter-example to (y)B(y,X), then
we can use it to generate a counter-example to (x)A(x,X). Clearly (2) is,
from an intuitionistic view, a stronger statement. Moreover it does not
require us to 'perform constructions on proofs' as the => in (1) does.
Furthermore, all of the theorems I have seen in constructive analysis sur-
vive translation from form (1) to form (2).

Since the formula in square brackets is a primitive recursive predicate, it
is uncontroversial to replace this statement by a first order approximation,
where instead of quantifying over X we quantify over finite approximations
to infinite sequences, which take the value 'undefined' for cofinitely many
arguments, and which can be p.r.-coded into natural numbers. Having done
this we get a statement

(3)          (x) (y) [ C (x,y) ]

For a particular x,y \in |N, (3) will evaluate to one of {true, false,
undefined}, because x is a partial function. So we can claim to have a
proof for (2) if we can prove that (3) always evaluates to either true
or undefined.

We can take *this* as proven if we give a proof in Heyting Arithmetic, say.
I'm not sure if all of HA is needed, though.

Actually I lied (whitely) above when I described the 'general form' for a
theorem in constructive analysis. Beyond the simplest theorems, they
actually say something like: There exists a construction \delta such that

(4)         (X) [ (x)A(x,X) => (y)B(y, X, \delta(X)) ]

But once the construction has been given (it is invariably primitive
recursive), we can plug it into (4) to get (1). So the proof of a statement
like (4) would consist of three parts: a construction \delta, a construction
 \gamma, and a proof in HA of a statement like (3).


SETS

We shall assume that a set of reals has the same degree of freedom as a
real: so that a set is given by a second-order object X and a formula A.
Thus Y \in S(X,A) iff (x) A(x,Y, X).

If we want to quantify over all sets in a particular domain, then we can do
so because the formula A can be encoded, so that we can use one
standard formula throughout. Call this formula G (for generic).
We are able to do this on the strength of the normal form theorem in
recursion theory (which is a perfectly constructive result, by the way).
Let me explain this:

By the normal form theorem for recursive functionals, applied here only
to primitive recursive functionals, there is a primitive recursive T and a
primitive recursive U such that for every primitive recursive A there is e
such that for every x, X, Y there is unique c such that T(c,e,x, X, Y)
holds, and A(x,Y,X) = U(c). Basically, c codes the finite computation
of A(x,Y,X). Thus if we want to quantify over all sets, we do so by
quantifying over all X and e above. We enfold the c variable into
the x variable, so in order to say

(S) ( ... Y \in S ... )

we write

(X, e) ( ... (x, c) (U(c) /\ (undefined if ¬ T(c,e,x,X,Y), true if
T(c,e,x,X,Y)) ... )

So we have a means of defining universal quantification over sets which
works like universal quantification over reals, a fact which enables
us to put theorems which talk about sets into the form (1).


CONCLUSION

I am pretty confident that all the constructive analysis laid out in Bishop
and Bridges is of the form outlined above, and so is reducible to
primitive recursive constructions and proofs in Heyting arithmetic. To my
mind this is an 'increase', albeit a slight one, in the constructive
credentials of this form of mathematics. For example it does away with
the somewhat ambiguous definition of sets in Constructive Analysis. It
has also bothered me that a constructive approach should make use of
reductio ad absurdum, and this method eliminates r.a.d. (because in
going from (1) to (2), we are basically saying that a contradictory state
of affairs points the way to one of our hypothesised objects not ful-
filling its defined requirements, rather than a flatly contradictory state
existing).

I have a lot more to say about why I think this way of looking at
constructive mathematics is philosophically clear, beneficial etc. But
I'll leave that for the time being.

Any thoughts welcome,

Jeremy Clark