Who First Proved that Peano Arithmetic is a Model of Computing (Turing Complete)?

[Charlie-Boo]

PA

1. If wff w(x) represents set P(x) i.e. w(x) is provable iff P(x) is true, then we can enumerate set P by generating all proofs and whenever w(x) is proven we enumerate x.

2. There is a wff w(x) that represents P(x) iff P is recursively enumerable.

Thus PA can enumerate the recursively enumerable sets.
Who first proved this? What is a good reference to such a proof?

PA and Turing Machines

Relation Q(Wff w with one free variable,the syntax for number N, Proof M) is defined to be Proof M proves w with N substituted for its free variable.

Relation R(Turing Machine M, the initial content C of its tape,iteration number N) is defined to be M started on C halts after exactly N iterations.

For every r.e. set S there is a w such that (exists A)Q(w,N,A) iff N is an element of S.
For every r.e. set S there is an M such that (exists A)R(M,N,A) iff N is an element of S.

Who first defined these relations and what is a good reference to this?

Note that we can also represent Q and R as being 2-place relations with the first component being the above first 2 components combined into one wff/Turing Machine.

I would guess Kleene and Smullyan but don't know of any particular references.

Thanks.

C-B

[Jeffrey Rubard]

It isn't. As per the *Handbook of Mathematical Logic* there are non-Turing-computable number-theoretic hyperfunctions.

[Charlie-Boo]

Of course there are non-recursive functions. But what does that have to do with PA being a Model of Computing?
Do you think that PA can't decide the recursive relations and enumerate the r.e. relations?
C-B

[Jeffrey Rubard]

"Effectively computable" = recursive. So non-recursive functions are not effectively computable.

[Charlie-Boo]

You are arguing that PA is stronger than Turing Machines.
(There's no need for me to argue against that.)
I have been told that the answer to my question is in fact Smullyan. Cheers.
"From R.M Smullyan, Recursion Theory for Metamathematics, OUP 1993, Ch. III "Shepherdson's Theorems":

<< At the time of Goedel's proof, the only known way of showing that all r.e. sets are representable in P.A. involved the assumption of omega-consistency. Well, in 1960, A. Ehrenfeucht and S. Feferman showed that all r.e. sets are representable in every *simply* consistent axiomatizable extension of the system (R). In fact, their proof showed the following stronger result:

**Theorem E.F.** If S is any simply consistent axiomatizable Rosser system for sets in which all recursive functions of one argument are strongly definable, then all r.e. sets are representable in S.

Their proof combined a Rosser-type argument with a celebrated result of John Myhill [...]
[Shortly after, strengthenings by Putnam, Smullyan, Shepherdson...] "