3
$\begingroup$

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?

  • 4
    $T_\text{tr}$ cannot possibly be recursively enumerable. If it were we could solve the halting problem: because, if $\phi$ is the assertion that some Turing machine $\mathfrak{M}$ halts, then either $\phi$ is in $T$ or $\lnot \phi$ is in $T$; so we could construct a Turing machine that searches for either $\phi$ or $\lnot \phi$ in $T_\text{tr}$, and this is guaranteed to halt.2012-11-28

2 Answers 2