# Semi-computable set of non-logical axioms implies semi-computable set of deductions

Question $$1$$ from Section $$7.7.3$$ in "A Friendly Introduction to Mathematical Logic" (Christopher C. Leary and Lars Kristiansen; $$2$$nd edition):

Let $$A$$ be a consistent set of $$\mathcal{L}_{NT}$$-axioms, and let

• $$U = \{\ulcorner\phi\urcorner \mid \phi \in A\}$$
• $$V = \{\ulcorner\phi\urcorner \mid A \vdash \phi\}$$

(a) Discuss the five assertions below. Which ones are true, and which ones are false?

[...]

(3) If $$U$$ is a semi-computable set, then $$V$$ is a semi-computable set.

A note about notation: The language (of number theory) $$\mathcal{L}_{NT}$$ is $$\{0, S, +, \cdot, E, \lt\}$$, where $$0$$ is a constant symbol, $$+$$, $$\cdot$$, and $$E$$ are $$2$$-ary function symbols, $$S$$ is a $$1$$-ary function symbol, and $$\lt$$ is a $$2$$-ary relation symbol (in this book, the equality symbol is a $$2$$-ary relation assumed always to be a part of a language). $$\ulcorner\phi\urcorner$$ denotes the Gödel number of the formula $$\phi$$.

Beyond stating what semi-computability means for the sets $$U, V$$ (i.e. that they are the domains of computable functions), and knowing that the assertion is true (the book states as much in the solution, but doesn't provide any details), I don't know how to approach proving the statement. Help would be welcome.

• Another way to think of semi-computable sets is to think of them as being enumerable (that’s why they are also called computably enumerable): so there is a machine that enumerates the elements in $U$. Given what logical entailment means (proofs are finite!), can you see how to use this? Aug 18 at 7:13

I'm not sure how formal a proof you're looking for, but here's one quick and informal way to see that this claim is true.

Say that $$U$$ is semicomputable. That is, there's a program $$M$$ so that we can run $$M$$ forever and eventually output exactly $$U$$. But after any finite amount of time, we have no way of knowing of $$M$$ is done executing yet.

We want to show that $$V$$ is semicomputable. That is, we would like to build a similar program $$N$$ which outputs $$V$$ at the end of time.

If you have some programming experience, it should be easy to see how to do this. Here's some incredibly sketchy pseudocode:

def N():
t = 1
while True:
U-approximate = "run M for t time steps"
V-approximate = "try all proofs of length at most t using the stuff in U-approximate"
print(V-approximate)
t += 1


Since every proof $$A \vdash \phi$$ is of finite length, using only finitely many things in $$A$$, this program will eventually output every such $$\phi$$. After all, we know $$M$$ semicomputes $$U$$, so for any finite subset $$A_0 \subseteq A$$ there will be a time $$t$$ after which $$M$$ outputs all of $$A_0$$ (do you see why?). So if $$A \vdash \phi$$ is a proof of length $$T$$, then after $$\max(t,T)$$ many times through the loop, $$N$$ will have output $$\phi$$.

I guess if you're being careful, you should also get the axioms from your logical system (in this case number theory) which will be another semicomputable thing to check. Then V-approximate should have access to these axioms as well as those coming from $$U$$.

Then an appeal to the church-turing thesis says that this code is really describing some computable function turning $$M$$ into $$N$$, which means $$N$$ really is semicomputable.

If you want to make this super precise, the main technical trick is the ability to run some preexisting program for some fixed number of steps $$t$$. This is actually a primitive recursive thing to do, in particular it's computable, and it's called the Kleene T Predicate.

With quite a bit of work, you can use this $$T$$ predicate, as well as encodings of the turing machine for $$U$$, in order to define a new turing machine for $$V$$ that correctly semicomputes the algorithm described above. I'll obviously be leaving this as an "exercise" (which I genuinely don't suggest you do :P).

I hope this helps ^_^

• The intuition for this claim now makes sense to me, but I'm also interested in the formal side of things. Could you perhaps outline the formal argument in more detail? Aug 18 at 8:59