[FOM] Church's Thesis Musings 2

[Harvey Friedman]

Continuation of http://www.cs.nyu.edu/pipermail/fom/2016-April/019740.html

Continued musings on Church's Thesis.

Again we will attack nondeterministic computation. We have a primitive
notion of structure on a finite set, isomorphism between them, and
induced substructure of a structure on a subset of its domain.

We have more primitives.  "nondeterministic program". Also a completed
computation under a given nondeterministic program. I.e., a structure
that encapsulates the entire record from initialization through
halting.

There are only finitely many structures of a given domain size up to
isomorphism.

There is an integer k such that any bijection between the domains of
two structures is an isomorphism if and only if its restriction to any
k element set is an isomorphism from the induced substructure on that
k element set onto the induced substructure of its image under that
restriction.

Under each program, there is an integer n such that the question of
whether a given structure is in fact a completed computation depends
only on the isomorphism types of its induced substructures of
cardinality n.

We will try to prove Church's Thesis in this form: the set all
completed computations is "recursive" in an appropriate sense. This
certainly can be levered in various philosophically coherent ways to
get lots of different forms of Church's Thesis.

So what this really amounts to is an abstract theory of finite
structures, induced substructures, isomorphisms, and "universal"
classes. The idea is to prove that the "universal" classes of
structures are "recursive". Thus this approach to proving Church's
Thesis is more general than computation.

I think I am beginning to understand the KEY mathematical idea here is
going to be. But I am still confused as to how I put this all together
into something philosophically coherent.

KEY MATHEMATICAL IDEA. The essence of a finite structure, is this. AN
EQUIVALENCE RELATION ON THE SUBSETS OF A GIVEN FINITE SET THAT
RESPECTS EQUINUMEROSITY. CALL THESE POWER EQUIVALENCES.

Not just any power equivalence. The integer k above figures
importantly. We want the condition that within a power equivalence,
two sets are equivalent if and only if there is a bijection between
them which sends k element subsets of the first to equivalent k
element subsets of the second. CALL THESE k-determined power
equivalences.

In a nondeterministic computation C, we have a generally infinite set
of k-determined power equivalences which, as a set, is n-determined.
Here k,n are functions of  C.

A set of power equivalences is n-determined if and only if membership
of a power equivalence depends only on its set of n element
restrictions (it is clear what these means for power equivalences), up
to isomorphism.

Obviously this is now mathematically completely well defined, and we
can easily prove that n-determined sets of k-determined power
equivalences are in fact recursive in all reasonable senses.

Now in order to start turning these musings into something
philosophically coherent, I need to prove the following.

CLAIM. The initial abstract formulation with those primitives provably
is entirely reflected in the power equivalence model. Hence Church's
Thesis is proved.

I'm still rather confused, but I think most of the ingredients are here.

BRUTE FORCE. This would be a good preamble. Argue - not with
conviction -  that finite structures are really power equivalence
relations, and isomorphism is as usual. You don't even need k here.
Just the n, as in an n-determined set of power equivalence relations.
Obviously you get recursiveness. But now try to be careful to talk
nicely about initialization and nondeterministic computation.

BEST. Prove that simple axioms about the primitives shows that the
Brute Force can be philosophically coherently applied to
nondeterministic computation in order to prove Church's Thesis. 

Harvey Friedman