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?
@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
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
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.