# Showing a set of true sentences is recursive

Let's assume we are working in $(\mathbb{N}, +, \dot\ , 0,1)$. Let $T$ be a set of formulae that is closed under $\neg$ and such that the set of Godel numbers of formulae in $T$ is recursive.

Moreover, let $\mathcal{A}$ be an axiomatic system that is valid (it only proves sentences $\varphi$ such that $\mathbb{N} \models \varphi$), and effective, and assume $\mathcal{A}$ is such that any true sentence in $T$ is also a theorem of $\mathcal{A}$.

I need to show that the set of true sentences of $T$ (their Godel numbers, technically speaking) is a recursive set.

Here's what I'm thinking, but I'm not sure about the details:

Since $\mathcal{A}$ is efective, any of its theorems can be obtained recursively, so, moreover, the set of true sentences of $T$ is then a recursively enumerable, which is half the battle towards showing it's recursive. Now, I'm not sure my reasoning is valid there, but even if it is, I still have to show that its complement is also recursively enumerable. I'm assuming somehow the fact that $T$ is closed under $\neg$ helps.

How do I proceed from here?

-

Let $S$ be the subset of true sentences in $T$. We can decide membership in $S$ in two steps:
1. If $\phi_n$ is not in $T$, then $\phi_n$ is not in $S$. (This uses the fact that $T$ is decidable!)
2. If $\phi_n$ is in $T$, concurrently search for a proof of $\phi_n$ and $\lnot \phi_n$ in $\mathcal{A}$; if we find a proof of $\phi_n$, then $\phi_n$ is in $S$, and if we find a proof of $\lnot \phi_n$, then $\phi_n$ is not in $S$.
This algorithm is guaranteed to halt because either $\phi_n$ is true or $\lnot \phi_n$ is true, and in either case, a proof of that fact can be derived from $\mathcal{A}$ since both $\phi_n$ and $\lnot \phi_n$ are in $T$.
Thanks a lot, Zhen, that does it. I understand your proof is enough, but out of curiosity, I'm wondering if it's possible to give explicit enumerations of both $S$ and $\mathbb{N}\setminus S$, in order to show $S$ is recursive? – FPP Sep 10 '12 at 20:13
@FPP, explicitly: For each $n\in\mathbb N$ do: (a) If $n$ is the Gödel number of a formula in $T$, then start over with the next $n$. (b) Print $n$ as a member of $\mathbb N\setminus S$. (c) If $n$ is not the Gödel number of a valid formal proof in $\mathcal A$, then proceed with the next $n$. (d) Let $\phi$ be the conclusion of the formal proof; if $\phi$ is not in $T$, then start over with the next $n$. (e) Print $\phi$ as a member of $S$. (f) If $\phi$ is of the form $\neg \psi$ and $\psi\in T$, then print $\psi$ as a member of $\mathbb N\setminus S$. (g) Start over with the next $n$. – Henning Makholm Sep 10 '12 at 20:54