FOM: Church's Thesis

[Vaughan Pratt]

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.

A witness to the failure of Church's Thesis can be a zero-knowledge
witness.  Zero-knowledge proofs have emerged recently as a concept of
foundational importance in computer science.  I gather from previous
discussions that f.o.m. is intended to be restricted to foundational
issues arising in the practice of mathematics, and since in practice fewer
mathematicians write zero-knowledge proofs than start from categorical
premises it would follow that zero-knowledge proofs are of even less
importance to the foundations of mathematics than category theory.

Vaughan Pratt