FOM: on constructivity

[William Tait]

In response to my question

>Is it impossible that, for example, there could be a classical but 
>no constructive proof of an existence statement yielding an 
>algorithm?


Fred Richman wrote


>I'm not sure this counts, but there are classical proofs of the
>existence of an algorithm with no corresponding constructive proofs in
>sight. Given any statement P, there is a classical proof of the
>existence of a (primitive recursive) function f such that f(n) = 1 for
>all n if P is true and f(n) = 0 for all n if P is false. Hartley
>Rogers gives an example of this type in "Theory of recursive functions
>and effective computability", with a footnote about excluded middle,
>constructivity, and intuitionists.


This is a classical proof of the existence of an algorithm for a 
total function with a certain property (constant 1 if P and constant 
0 if not-P). But the proof does not yield such an algorithm (i.e. 
does not give an algorithm for finding such an algorithm).

A more interesting kind of example is this: let f(n) = 1 if no proof 
of length <= n is found of the inconsistency of ZF and let f(n) = 0, 
otherwise. There is an algorithm for f, but only classically can we 
prove that f is total. On the other hand, classically we can assert 
that there is another algorithm for the same function which is 
constructively total.

Is it possible that there is an e such that classically {e} is total 
and such that, for no e' is {e'} constructively total and 
(classically) = {e}?

Incidentally, I want to apologize for the `metaphor and hot wind' 
remark (and what followed) in my original posting (7/11/00) in 
response to Dirk van Dalen. It was meant to express enthusiasm for 
arguing the point, not ill-temper or contempt.

Bill Tait

-- 
William W. Tait
Professor Emeritus of Philosophy
University of Chicago
wwtx at midway.uchicago.edu
Home:
5522 S. Everett Ave
Chicago, IL 60637
(773) 241-7288