How to prove that the set of theorems of any recursively axiomatized theory is a recursively enumerable set?

67 Views Asked by At

I read the article Craig's theorem written by Putnam (1965). I don't understand the claim on page 3 of the article:

The set of theorems of $T$, where $T$ is any recursively axiomatized theory, is also a recursively enumerable set. The idea of the proof is to arrange all the proofs in $T$ in an effectively produced sequence (say, in order of increasing number of symbols). If one replaces the $i$th proof in the resulting sequence $\text{Proof}_1,\text{Proof}_2,\dots$ by the wellfounded formula that is prroved by $\text{Proof}_i$, one obtains a listing of all and only the theorems of $T$.

However, this section doesn't provide a detailed explanation.

Of course intuitively, at first glance, since a proof must have a finite length, and the set of axioms is recursive, we obtain that the proofs are enumerable, since we have decidable procedures about elements of the set of axioms and can count each step of the proofs.

However, that is just informal thinking. So how do we know that "the set of theorems of any recursively axiomatized theory is a recursively enumerable set?"

1

There are 1 best solutions below

0
On BEST ANSWER

We have a theory $T$ that is recursively axiomatisable, so the list of axioms of that theory is recursive. Proofs, in our proof system, are finite lists of formulae $\langle\phi_0,\phi_1,\dots,\phi_n\rangle$, under some deduction or inference rules. These inference rules are all recursive. That is, if you give me a proof $\langle\phi_0,\dots,\phi_{n-1}\rangle$ and another formula $\phi_n$, then it is decidable if $\langle\phi_0,\dots,\phi_n\rangle$ is also a valid proof.

Now, we can enumerate all wellformed formulae in the language of $T$ in a recursive way, so let us do that as $\{\phi_i\mid i\in\mathbb{N}\}$. Now we can produce a list of all finite lists of these formulae in a recursive way. For example, we can use prime factorisations, so the $2^i\times3^j\times5^k$th element of the list is $\langle\phi_i,\phi_j,\phi_k\rangle$. Lets call this $\{S_i\mid i\in\mathbb{N}\}$, where each $S_i$ is a string of wellformed formulae.

Now we can recursively enumerate the list of proofs as follows: Let us suppose that we have already listed proofs $P_0,P_1,\dots,P_n$. Then first we look for $P_n$ in our list of all strings. Suppose that $P_n=S_i$. Then we look at $S_{i+1}$ and decide if it is a valid proof. This is a decidable process as we have discussed, so in finite time we can conclude if $S_{i+1}$ is a valid proof. If it is, then we set $P_{n+1}=S_{i+1}$. Otherwise, we move on to $S_{i+2}$, etc.

We now have a recursively enumerated list of all valid proofs from $T$, let us call it $\{P_i\mid i\in\mathbb{N}\}$. Given a proof $P_i$, let $\psi_i$ be the final element of the string (this process is computable). Then $\{\psi_i\mid i\in\mathbb{N}\}$ is a recursively enumerated list of theorems of $T$ (since each one comes from a proof from $T$). Furthermore, any theorem $\psi$ of $T$ must have a proof, and so $\psi=\psi_i$ for some $i$. Hence, we have recursively enumerated all theorems of $T$.