Re: Are open formulae really needed?

From: Daryl McCullough (stevendaryl3016_at_yahoo.com)
Date: 01/30/05 

Date: 30 Jan 2005 06:29:59 -0800

David C. Ullrich says...

>Take the Riemman Mapping Theorem in complex analysis:
>
>Thm. If D is a simply connected subdomain of C and D <> C then
> D is conformally equivalent to the unit disk.
>
>Note first that the statement of the theorem contains both
>free variables and constants: It doesn't begin with
>"for every D...", and it uses the notations "C" and
>"the unit disk" instead of inserting definitions of same.
>
>Now what does the actual proof look like? If the author
>is more careful about these sorts of issues than many
>people the proof begins "Suppose that D is a simply
>connected subdomain of C and D <> C." Many authors
>omit that sentence, but they then give the proof
>as though it had been written at the start.
>
>In particular the proof does _not_ consist of a
>sequence of sentences with no free variables,
>with _every_ line of the proof beginning
>"for all D, if D is a simply connected subdomain
>of C and D <> C then ..."

Constructive type theorists point out that there is
an exact analogy between the use of free variables
in a proof and the use of additional hypotheses. If
you are wanting to prove that something follows from
the continuum hypothesis, then you *don't* write a
proof in which every line is of the form

    If the continuum hypothesis is true, then ...

You just announce at the beginning that you are assuming
CH, derive your result, and then discharge the hypothesis
to get

    CH -> whatever

In constructive type theory, the use of free variables
is exactly like the use of hypotheses; at any step in
a proof, you have an implicit "context" which consists
of the variables introduced and the assumptions made
about them. 

--
Daryl McCullough
Ithaca, NY
Quantcast