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?