[FOM] Church's Thesis Musings

[Harvey Friedman]

I claim that we don't have a ZFC like entity in computation quite yet.
The way I was talking about it above really says that a ZFC like entry
amounts fundamentally to the core of an arguable proof of Church's
Thesis. According to the analogy you are making, Church's Thesis is
viewed as being solved by TMs. This goes against the grain of most of
the philosophically minded people who today look at computation.
Namely, that there really is a foundational challenge left with this
so called "Church's Thesis". I agree with the conventional wisdom on
this, and do spend some time trying to prove Church's Thesis.

TM's just are not sufficient for this in 2016. ZFC is arguably in the
ball game for math formalization, and sugared ZFC is by far the best
that we have. So called alternative general purpose foundations do not
represent the kind of progress needed for Zermelo's Thesis, or
whatever you want to call it.

I have tried the following ideas over the years, and I never had the
patience to really see it through so that it is totally convincing.

I will now try to restart my efforts armed with the benefit of being older.

I now think that nondeterministic computation is more tractable. After
nondeterministic Church's Thesis is proved, a lot can be done to
transfer it to a proof of (deterministic) Church's Thesis with high
philosophical standards.

1. In a nondeterministic computation, there is going to be discrete
stages, starting with initialization. We seek a finite path to halting
from the initialization. The goal is to prove that the set of
initializations that start a path ending with halting is r.e. in the
usual technical sense.

2. Every stage of computation is COMPLETELY represented by a finite
structure up to isomorphism (the current state of the system). There
is no memory. Any memory must be embodied in the present structure
(state). Only isomorphism types are meaningful.

3. The issue boils down to: what the admissible pairs of finite
structures, M,M', are. These are called the transition relations on
finite structures.

4. At this point, one normally would require that the finite
structures have a certain standard form, like sugared digraphs, and
talk about principles of locality. Yes, that will work and be modestly
convincing. But we really need something better.

5. In particular, we need a new principle of locality that completely
transcends any precise way of representing these finite structures
M,M'. This is where I always get stuck. Perhaps age will come to the
rescue.

6. By the way, there are some old attempts by Gandy in this direction,
and Sieg took some of them up. I think Sieg has gotten discouraged at
some point about this line of attack on Chuch's Thesis. Also Gurevich
and Dershowitz have an approach. Anyway, let's bull forward.

7. There is a notion of substructure and size of structures. If we are
working with graphs, then I think we should be thinking induced
subgraphs and numbers of vertices. But we don't want to commit
ourselves to graphs.

8. One really simple idea, which I can see arguments both for and
against, is this. The only thing that counts in a nondeterministic
computation is the sets of small substructures. I.e., if M is a finite
structure then the set of admissible continuations M' off of M respect
the equivalence relation of k-equivalence.

9. Let me be a little more specific. M,M* are k-equivalent if and only
if they have the same <= k sized localizations up to isomorphism. So
in a nondeterministic computation, we have the following principle of
locality:

Suppose M,M* is a legitimate state transition. Suppose M,M' are
k-equivaelnt, and M*,M*' are k-equivaelnt. Then M*,M*' is a legitimate
state transition.

10. The condition to be placed on nondeterministic computation is that
there exists a number k such that the condition in 9 holds with k.
This is still not quite enough to conclude that we are staying with
the r.e. sets. But we are getting close.

11. There is an objection to this approach. That is, that in a state
transition, it is not only the M,M' as two things, but how M relates
to M'. This suggests that we consider the join of two finite
structures, (M,M'). And then there is the idea of substructures of
this join, and k-equivalence between these joins. This seems
philosophically manageable.

12. The new idea needed to push this through is an abstract treatment
of little induced substructures of a structure. It has to be done with
great finesse without committing to any specific features of any
embodiment of finite structures like graphs, digraphs, or relational
structures in model theory, etc. THIS IS TOTALLY DOABLE. Like to hear
in detail from anybody who claims that they have done this just
right.

Harvey Friedman