Posts's Theorem

Published May 19, 2022  -  By Marco Garosi

Post’s Theorem, named after Emil Post, is a theorem in the computability theory that gives a characterization of recursive sets. Indeed it states that a set is recursive if and only if it and its complement (namely Aˉ=NA\bar{A} = \N \setminus A ) are recursively enumerable (r.e.).


We can rewrite formally what we’ve just said:

A recursive     Ar.e. Aˉr.e. A \text{ recursive } \iff A \in \text{r.e. } \land \bar{A} \in \text{r.e.}

Post's Theorem


Let ANAˉ=NAA \subseteq \N \land \bar{A} = \N \setminus A.

Similarly to what we do to prove Rice’s Theorem, we have to prove the double implication.

Left to right,     \implies

Let’s assume that AA is recursive. Then it must have a characteristic function fAf_A, which is total and recursive.

Let’s define:

Ψ(x)={1if fA(x)=1 (xA)otherwise \Psi(x) = \begin{cases} 1 &\text{if } f_A(x) = 1 \text{ } (x \in A) \\ \uparrow &\text{otherwise} \end{cases}

Function Ψ\Psi is partial (it does not always halt) and recursive; it is the semicharacteristic function of AA.

You can construct an analogous function for Aˉ\bar{A}. In fact, you could define fAˉ=1fAf_{\bar{A}} = 1 - f_A.

Since AA and Aˉ\bar{A} have a semicharacteristic, partial recursive function Ψ\Psi, they are recursively enumerable (r.e.).

Right to left,     \impliedby

Let’s assume that AA and Aˉ\bar{A} not be r.e., with semicharacteristic functions ΨA\Psi_A and ΨAˉ\Psi_{\bar{A}}. Hence we can define:

fA={1if ΨA(x)0if ΨAˉ(x) f_A = \begin{cases} 1 &\text{if } \Psi_A(x) \downarrow \\ 0 &\text{if } \Psi_{\bar{A}}(x) \downarrow \end{cases}

Since AA and Aˉ\bar{A} are complementary, then xAxAˉx \in A \lor x \in \bar{A}. So, function fAf_A always returns a value, as long as ΨA\Psi_A and ΨAˉ\Psi_{\bar{A}} are run in parallel on interleaving (one instruction of ΨA\Psi_A and one of ΨAˉ\Psi_{\bar{A}}). Running them in such a way prevents one function diverging from blocking the other — no blockings are created.

Function fAf_A, then, is total recursive; AA is thus recursive by definition. \square

Share on: