[FOM] 203:Proof(?) of Church's Thesis - Restatement

[Harvey Friedman]

The treatment of transition of global states in 202:Proof(?) of Church's
Thesis, (and also see Comment on Church's Thesis 12/31/03 12:17AM) are
missing a key additional idea. As they stand they are too weak, but are on
the right track. In fact, they are so weak that they do not allow algorithms
to force the creation of new locations. (So these presentations, as they
stand, are deeply flawed).

The essence of the matter is the handling of "transition" functions F from
finite systems into finite systems. The previous idea is that the
isomorphism type of the "transition system"

(M,F(M))

should depend only on the isomorphism type of M, and should obey a "uniform
finiteness" condition (error numbers). But there is a key missing idea.

The missing idea surrounds the issue of how the new locations created during
computation, relate to the old locations. I.e., how does dom(F(M))\dom(M)
relate to M?

What is crucially needed is a richer notion of transition system. A
transition system should augment M,F(M) with a system of partial functions
from dom(M) which generate the new locations - i.e., elements of
dom(F(M)\dom(M). 

In deterministic computation, the isomorphism type of the "transition
system"

(M,F(M),f1,...,fp)

should depend only on the isomorphism type of M, and there should be the
same "uniform finiteness" condition. After the transition, only F(M)
survives (as the new global state).

Recall that the uniform finiteness condition I used depends on the notion of
restriction of systems (M,F(M)). Here we use the appropriate notion of
restriction of transition systems, which, because of the use of the partial
generating functions, takes on an "enhanced" character. This is what allows
algorithms, in this model, to force the creation of new locations with
controlled relationships with the old locations, as well as with themselves.

An added bonus of this new ingredient - the generating functions in
transition systems - is that it also gives an upper bound on the growth of
locations during computation. This makes the adaptation of these ideas to
computational complexity more natural.

We restate this approach using this crucial new ingredient.

The style of presentation will be different. I will be very explicit about
the mathematical content of this model of computation, with only brief
remarks about philosophical considerations. Right now, the main issue is
just how good this model is, in terms of addressing the philosophical
problem. Actually making this philosophically convincing, or tweaking it to
make it more philosophically convincing, can be taken up later.

*************************************

RESTATEMENT.

There is a considerable amount of literature on Church's Thesis, some of
which is recent. I certainly have not absorbed this literature, and so I
offer this approach with the expectation that others who have thought about
this and/or written about this will explain their ideas here on the FOM.

If what I say here turns out to be, to various degrees, "known", then I
offer this as a clear and concise and friendly and public exposition.

We will propose a condition on deterministic computation which appears to us
to be capable of being made compelling to a degree which corresponds roughly
to the length and care of the accompanying prose. However, we limit the
length and care of any accompanying prose here.

As is usual when discussing the classical Church's Thesis and classical
variants, we assume that computation proceeds along a discrete time axis
numbered 0,1,2,3,... . We also assume that at each stage n >= 0 of
computation, there is a well defined finite "system" that provides the
"global state" at that stage. Also that these systems are "exact". I.e.,
that there is no vagueness or randomness about what the finite structure is
at any stage of computation.

Any given algorithm must at least specify the following information, which
we present informally.

1. The "features" of the global states.
2. Which global states are terminal.
3. What the next global states are, if any, that are allowed to follow a
given global state. I.e., the global transition relation S. We may also
impose a deterministic condition.
4. How M' relates to M. In particular,
5. how M,M' must fit together, taking into account the overlap between the
domain of M and the domain of M'.
6. and how the elements of dom(M')\dom(M) are generated from the elements of
dom(M).

All global states used in the implementation of all algorithms will be
"finite systems" of the form M = (D,R1,...,Rk), where

i) D is a finite set (of locations);
ii) k >= 1;
iii) the R's are relations on D of various arities >=  1 - i.e.,
relationships between locations.

The type of M is the sequence of arities n1,...,nk, of the R's.

In order to avoid extraneous issues about the unlimited character of
elements of D, so that the development here is well within the usual axioms
of even finite mathematics, we will assume that every element of D is an
hereditarily finite set. This causes no loss in generality, as all
significant matters will be invariant under isomorphism.

The passage from one global state to another is represented by what we call
"finite system transitions" of the form

T = (D,R1,...,Rk,D',R1',...,Rk',f1,...,fp)

where (D,R1,...,Rk) and (D',R1',...,Rk') are finite systems of the same
type, and each fi is a partial function from D into D'\D of some arity ai,
such that the union of the ranges of the fi is D'\D. Thus D'\D is
"generated" by the partial functions f1,...,fp from D.

The type of the finite system transition T is written as (sigma,sigma,tau),
where sigma is the type of (D,R1,...,Rk), and tau is the sequence of arities
of the f's. 

The source size of the finite system transition T is the cardinality of D.

We now become more formal about global transition relations. We first define
a very general notion of (nondeterministic and deterministic) global
transition relation. We then put a condition on global transition relations
that allows us to deduce that their behavior is effective in the sense of
recursion theory.

A global transition relation consists of a set S of finite system
transitions, satisfying certain conditions.

1. There is a type (sigma,sigma,tau) of finite transition systems such that
every element of S is of this type.
2. Any finite transition system isomorphic to an element of S is an element
of S.

This is the nondeterministic case. We will address the deterministic case
later.

We now come to the crucial finiteness condition on S.

FINITENESS CONDITION ON S. There is a positive integer n such that the
following holds. Let T be a finite transition system not lying in S. Then
there exists a restriction T' of T whose source size is at most n, which is
not a restriction of any element of S.

We need to explain the notion of restriction. Let T be a finite transition
system of type (sigma,sigma,tau). Write

T = (D,R1,...,Rk,D',R1',...,Rk',f1,...,fp).

The restrictions of T are are the

(E,R1|E,...,Rk|E,D*,R1'|D*,...,Rk'|D*,f1|E,...,fp|E)

where E is a subset of D, and D* is the union of E and the ranges of
f1|E,...,fp|E. It is obvious that these restrictions are finite transition
systems of type (sigma,sigma,tau), whose source size is the cardinality of
E.

Before discussing the idea behind this finiteness condition, we need to
remark on how the global transition relation S relates to nondeterministic
computation.

Each element T of S tells us that if we are in the global state represented
by the first sigma part of T (which is a finite system of type sigma), then
we are allowed to transition to the second sigma part of T (also a finite
system of type sigma). The tau part of T comes into the picture as an
allowable way of creating the new locations.

Nondeterministic computation proceeds by first choosing an initial global
state in the form of a finite system of type sigma, and then
nondeterministically transitioning according to the previous paragraph.

The idea behind this finiteness condition on S is the following. Suppose T
does not lie in S. Then T is incompatible with the nondeterministic
algorithm. I.e., the proper relationships between locations, new and old,
were violated. The second sigma and the tau part of T represents a way of
transitioning from the first sigma part of T - the source. Because
algorithms are broken down to operate locally, as can be seen by their
content, we see that this violation must have been generated by at most a
fixed number of locations in the source (the first sigma part of T). Thus we
can find a localized violation. This localized violation cannot be papered
over in any way through the addition of locations, and remains as long as
this localized part is present.

THEOREM 1. Let S be a global transition relation. Then the relation of one
global state being reachable from another using S, is recursively enumerable
in the sense of recursion theory. Furthermore, for any finite type sigma,
every transitive recursively enumerable relation between finite systems of
type sigma is the reachability relation for some global transition relation
based on some (sigma',sigma',tau), where sigma' is an expansion of sigma, in
an appropriate sense involving reducts.

We say that a global transition relation S is deterministic if and only if
whenever T,T' lie in S and have the same first sigma parts, there is an
isomorphism from T onto T' that is the identity on the domain of the first
sigma parts.  

Theorem 1 tells us that we can simulate nondeterministic computation in the
sense of recursion theory, with global transition relations.

THEOREM 2. (Informal statement). We can simulate deterministic computation
in the sense of recursion theory, with deterministic global transition
relations.     

The proof of these Theorems are technically straightforward. The
contribution here, if any, is the recognition that the core technical idea
(straightforward) can be adapted to provide an approach to Church's Thesis.
Of course, I looked for such a core technical idea, not knowing whether it
would be straightforward or not in advance.

NOTE: This approach suggests certain formal models of computation that have
probably not been studied, and which are very powerful and very natural in
their own right. We can study just how minimal sigma and tau can be, as well
as the error number n, so that the usual Turing completeness phenomena kicks
in. I expect that the inherent computation power is tremendous, so that
sigma, tau, n can be taken to be strikingly minimal.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 201st in a series of self contained numbered postings to
FOM covering a wide range of topics in f.o.m. The list of previous
numbered postings #1-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM

Harvey Friedman