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

Question

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.

Answer 1

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 ^_^