For every recursively enumerable set P(x) there is a wff W(x) with one free variable x that represents P i.e. P(x) is true iff W(x) is provable in PA.

Who first proved this and what are popular (standard) and recent references (book or website) that give this fact?

C-B

On Tuesday, 16 November 2021 at 15:35:18 UTC+1, Charlie-Boo wrote:
>
> For every recursively enumerable set P(x) there is a wff W(x) with one free variable x that represents P i.e. P(x) is true iff W(x) is provable in PA.
>
> Who first proved this and what are popular (standard) and recent references (book or website) that give this fact?

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...] >>

BTW, you are in the wrong group: that is mathematical logic, not computer science.

HTH,

Julio