Question about computability of true/provable formulas I would like to clarify some things related to the computability of the sets of all theorems and true formulas for the formal arithmetic.
Consider the theory $T$ of formal arithmetic (the theory of natural numbers with the usual notation of successor, addition...). And define the sets


*

*$T_{th}$ all  theorems of $T$

*$T_{tr}$ all statements of $T$ that are true under the standard interpretation.


It appears to me that both sets are recursively enumerable. For $T_{th}$ we can easily construct a Turing machine $T$ that given a formula $\varphi$ generates all possible proofs and checks if they prove $\varphi.$ In the same manner one could make a Turing machine for $T_{tr}$ that finds (if exists) the proper interpretation of the supplied formula and thus verify if its true under the standard interpretation.
However neither set is recursive. Assuming $T$ is consistent we have (by Godels's theorem) a formula $\varphi$ so that $\varphi \not \in T_{th}$ and also $\varphi \not \in T_{th}$ and so there can be no algorithm that recognizes elements of $T_{th}$ and halts on $\varphi.$
To see that $T_{tr}$ is not recursive we can check the results related to Hilberts tenth problem which can be re-phrased to deal with natural numbers.
What I am now wondering is if the above reasoning is correct? Am I missing something? Is there something to add?
 A: @Zhen Lin's comment should really be promoted to an answer: he gives one good snappy argument. Here just for fun is another cute variant argument, depending on a Very Basic Theorem about effectively enumerable sets. [If you prefer, substitute 'recursively enumerable' throughout -- but the argument flies even deploying a more informal notion of effective enumerability.] 
We are going to show, then, that

The set of truths of a sufficiently expressive language $L$ is not effectively enumerable.

Here a 'sufficiently expressive' language is one that can (i) express every effectively computable one-place numerical function, and (ii) can form wffs which quantify over numbers.
Proof  Take the argument in stages. (i) The Very Basic Theorem about e.e. sets of numbers which I alluded to tells us 

There is a set $K$ which is e.e. but whose complement $\overline{K}$ isn't. 

Let's take that as proved. And now suppose the effectively computable function $k$  enumerates such a set $K$, so $n \in K$ iff $\exists x\,k(x) = n$, with the variable running over numbers. 
(ii) Since $k$ is effectively computable, in any given sufficiently expressive arithmetical language $L$ there will be some wff of $L$ which expresses $k$: let's abbreviate that wff  $\mathsf{K(x,y)}$. Then  $k(m) = n$ just when $\mathsf{K(\overline{m},\overline{n})}$ is true.
(iii) By definition, a sufficiently expressive language can form wffs which quantify over numbers. So $\exists x\, k(x) = n$ just when $\mathsf{\exists x(\mathsf{Nat(x)} \land  \mathsf{K}(x, \overline{n}))}$ is true (where $\mathsf{Nat(x)}$ stands in for whatever $L$-predicate might be needed to explicitly restrict $L$'s quantifiers to numbers).
(iv) So from (i) and (iii) we have $n \in K$ if and only if $\mathsf{\exists x(\mathsf{Nat(x)} \land 
 \mathsf{K}(x, \overline{n}))}$ is true; therefore,  $n \in
 \overline{K}$ if and only if $\mathsf{\neg\exists x(\mathsf{Nat(x)}
 \land  \mathsf{K}(x, \overline{n}))}$ is true.
(v) Now suppose for a  moment that  the set $\mathcal{T}$ of true sentences  of $L$ is effectively enumerable. Then, given a description of the expression $\mathsf{K}$, we could  run through the supposed effective enumeration of $\mathcal{T}$, and whenever we come across a truth of the type $\mathsf{\neg\exists x(\mathsf{Nat(x)} \land  \mathsf{K}(x, \overline{n}))}$ for some $n$ -- and it will be effectively decidable if a wff has that particular syntactic form -- list the number $n$. That procedure would give us an effectively generated list of all the  members of $\overline{K}$. 
(vi) But by hypothesis $\overline{K}$ is not effectively enumerable. So  $\mathcal{T}$ can't be effectively enumerable after all. Which is what we wanted to show.
A: The complexity of both of these sets is very well understood.


*

*$T_{th}$, the set of theorems of Peano Arithmetic, is Turing equivalent to the halting problem. As you said: given a formula, we can write a program to search for a proof; using the halting problem, we can tell whether this program halts. So if we can tell which programs halt, we can tell which formulas are provable. Conversely, given a program, we can write a formula saying that the program halts. This formula will be of a particular syntactic form ($\Sigma^0_1$), and a formula with that special form is provable in PA if and only if it is true. So if we can tell which formulas are provable in PA, we can tell which programs halt.

*$T_{tr}$, the set of true formulas of PA in the standard interpretation, is Turing equivalent to the set $\emptyset^{(\omega)}$, the $\omega$-th Turing jump of the empty set. In particular, this set is not definable by any formula in the language of Peano arithmetic.
