FOM: on constructivity
William Tait
wwtx at midway.uchicago.edu
Wed Jul 19 10:42:30 EDT 2000
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
More information about the FOM
mailing list