FOM: Church's Thesis

[Stephen Fenner]

On Fri, 17 Sep 1999, Vaughan Pratt wrote:

> 
> Shipman:
> >My point was that if we could KNOW that Church's Thesis is false, it
> >would be in the context of some mathematized physical theory within
> >which one could derive an experimental procedure for calculating a
> >noncomputable sequence; and the sequence would be definable within this
> >mathematized theory and presumably within ZFC.
> 
> Certainly.  But while you're waiting for this witness to the failure of
> Church's Thesis to materialize, I already have in front of me a sequence
> of two bits the first of which encodes the truth of Con(ZFC) and the
> second its negation.  This is a well-defined sequence, the consistency
> of ZFC being well-defined.  Do I therefore know the truth of Con(ZFC)?
> Unfortunately no as actually I have two well-defined sequences in front
> of me, 01 and 10.  Damn.
> 
> If and when a well-defined uncomputable sequence ever materializes,
> will we then know any more about Con(ZFC)?  No, because we'll then also
> possess every recursive permutation of that sequence, all of which will
> be well-defined uncomputable sequences.  We'll then be confronted with
> an infinite shell game yielding no more information than my finite one.
> 

I think what Joe might mean (correct me, Joe) is that if we find that
Church's Thesis is false, it will come from a physical theory (expressed
mathematically) which not only allows us to build a physical device 
to compute some definable
non-Turing computable sequence, but also GIVES US a concrete definition of
the sequence as well, so that one could conceivably infer from this
definition that Con(ZFC) is
coded in, say, its 217th bit (a low-ball estimate).  If the device is run
long enough, then more bits would emerge, but we need only run the device
a finite amount of time to get the 217th bit.

Of course most noncomputable sequences give no useful information at all
(arithmetically random, generic).

Stephen Fenner                       Phone: 803-777-2596
Computer Science Department          FAX:   803-777-3767
University of South Carolina         Email: fenner at cs.sc.edu
Columbia, SC  29208  USA             Web:   http://www.cs.sc.edu/~fenner