[FOM] Simple Turing machines, Universality, Encodings, etc.

[Francis Davey]

joeshipman at aol.com wrote:

> PCE doesn't need to be precise to be refutable. All one needs to do to 
> refute it is produce a process which
> 

I apologise if these seems like an ignorant suggestion, but isn't
something like Girard's "system F" a reasonable candidate.

For those not familiar with it, system F (or the "polymorphic lambda 
calculus" as it is sometimes known) is a language with rules for 
term-rewriting that are strongly normalising. System F can represent a 
very wide class of functions (including all that are provably 
terminating in second order peano arithmetic) but it is not universal. 
The proof that it is not universal is complicated and (to me) far from 
obvious.

Its not usually defined as a cellular automaton, but surely a cellular 
automaton with the properties of system F could be transparently created?

Looking at the criteria.

> i) is simpler to define than Wolfram's "universal" examples

Is of course subjective since "simplicity of definition" is a difficult
concept to formalise and is likely to be definition dependent, but it
seems to me that system F is fairly simple to define, if not trivial.

> ii) does not obviously fail to be c.e.-complete

If I understand this correctly (and maybe I don't), it does not
*obviously* fail to be c.e.-complete unless you have a very
sophisticated concept of obviousness.

> iii) is nonetheless provably not c.e.-complete

but yet it is not.

I would be interested to know where my thought processes have gone wrong
here.

-- 
Francis Davey
169 Temple Chambers, 3-7 Temple Avenue, London EC4Y 0DA
Tel. 020 7583 7644  Mobile. 0781 686 8998 Fax. 020 7353 8554