[proofplan] We prove the equivalence using the separator formulation of [PA degrees](/page/PA%20Degree): a complete consistent extension of PA computes a separator for every pair of disjoint computably enumerable sets. This separator is then used to choose an infinite branch through any infinite computable binary tree. Conversely, we build a genuinely prefix-closed computable tree of bounded finite PA-completions; any path through it computes a complete consistent extension of PA. Finally, nonempty $\Pi^0_1$ classes in Cantor space are exactly path sets of infinite computable binary trees. [/proofplan]

[step:Fix representatives and reduce degree language to oracle computations] Let $A \subseteq \mathbb{N}$ be a representative of $a$, so $\deg_T(A)=a$. Since Turing reducibility is invariant under Turing equivalence, a set computable from one representative of $a$ is computable from every representative of $a$. Thus, throughout the proof, it is enough to prove the assertions with respect to this fixed oracle $A$. We write $2^{<\mathbb{N}}$ for the set of finite binary strings. For $\sigma,\tau \in 2^{<\mathbb{N}}$, write $\sigma \preceq \tau$ when $\sigma$ is an initial segment of $\tau$. If $T \subseteq 2^{<\mathbb{N}}$ is a tree, define its path set \begin{align*} [T] := \{X \in 2^{\mathbb{N}} : X{\upharpoonright}n \in T \text{ for every } n \in \mathbb{N}\}. \end{align*} Here $X{\upharpoonright}n \in 2^{<\mathbb{N}}$ denotes the initial segment of $X$ of length $n$. [/step]

[step:Show that a PA degree computes separators for disjoint computably enumerable sets]Assume that $a$ is a PA degree. Then $A$ computes a complete consistent extension $C \subseteq \mathbb{N}$ of PA, where $C$ is coded as the set of Gödel numbers of sentences belonging to the theory. Let $U,V \subseteq \mathbb{N}$ be disjoint computably enumerable sets. Fix monotone cumulative computable enumerations \begin{align*} u: \mathbb{N} &\to \mathcal{P}_{\mathrm{fin}}(\mathbb{N}),\\ v: \mathbb{N} &\to \mathcal{P}_{\mathrm{fin}}(\mathbb{N}), \end{align*} where $u(s)$ and $v(s)$ are the finite sets enumerated into $U$ and $V$ by stage $s$, with $u(s) \subseteq u(s+1)$ and $v(s) \subseteq v(s+1)$ for every $s \in \mathbb{N}$. For each $n \in \mathbb{N}$, let $\theta_n$ be the arithmetical sentence saying that $n$ enters $U$ before it enters $V$: \begin{align*} \theta_n \equiv \exists s \Bigl(n \in u(s) \text{ and } \forall t \leq s\, n \notin v(t)\Bigr). \end{align*} The relation inside the quantifier is decidable, so PA represents it. Define \begin{align*} S_C := \{n \in \mathbb{N} : \ulcorner \theta_n \urcorner \in C\}. \end{align*} Since $C \leq_T A$, the set $S_C$ is computable from $A$. If $n \in U$, then because $U$ and $V$ are disjoint, $n$ enters $U$ at some first stage before it ever enters $V$. PA proves the corresponding true bounded computation, hence PA proves $\theta_n$, and therefore $\theta_n \in C$. Thus $U \subseteq S_C$. If $n \in V$, let $s_0$ be the first stage at which $n$ enters $V$. Since $U$ and $V$ are disjoint, PA proves the bounded facts that $n \notin u(t)$ for every $t < s_0$ and that $n \in v(s_0)$. For $s < s_0$, the first bounded fact rules out the conjunct $n \in u(s)$; for $s \geq s_0$, the second bounded fact and monotonicity of the enumeration of $V$ imply that the conjunct $\forall t \leq s\, n \notin v(t)$ fails. PA therefore proves that no $s$ witnesses $\theta_n$, so PA proves $\neg\theta_n$. Since $C$ is consistent, $\theta_n \notin C$, so $n \notin S_C$. Hence $S_C \cap V = \varnothing$. Therefore $A$ computes a separator $S_C$ satisfying \begin{align*} U \subseteq S_C \quad\text{and}\quad S_C \cap V = \varnothing. \end{align*}[/step]

[guided]The point of this step is to extract from a complete consistent theory a uniform choice procedure for any disjoint computably enumerable pair. Let $U,V \subseteq \mathbb{N}$ be disjoint computably enumerable sets, and fix monotone cumulative computable stage-by-stage enumerations \begin{align*} u: \mathbb{N} &\to \mathcal{P}_{\mathrm{fin}}(\mathbb{N}),\\ v: \mathbb{N} &\to \mathcal{P}_{\mathrm{fin}}(\mathbb{N}). \end{align*} Thus $u(s) \subseteq u(s+1)$ and $v(s) \subseteq v(s+1)$ for every $s \in \mathbb{N}$, and $n \in U$ means that $n \in u(s)$ for some stage $s$, with the analogous statement for $V$. For each $n \in \mathbb{N}$, define the sentence $\theta_n$ to mean: "$n$ enters $U$ before it enters $V$." Formally, \begin{align*} \theta_n \equiv \exists s \Bigl(n \in u(s) \text{ and } \forall t \leq s\, n \notin v(t)\Bigr). \end{align*} The matrix of this formula is decidable because it only asks about finitely many computable enumeration stages. Hence PA can verify any true bounded instance of it. Now define \begin{align*} S_C := \{n \in \mathbb{N} : \ulcorner \theta_n \urcorner \in C\}. \end{align*} Because $A$ computes the complete theory $C$, it also computes $S_C$: on input $n$, compute the Gödel number $\ulcorner\theta_n\urcorner$ and ask whether it belongs to $C$. We verify that $S_C$ separates $U$ from $V$. Suppose first that $n \in U$. Since $U$ and $V$ are disjoint, $n$ never enters $V$. At the first stage $s$ where $n$ enters $U$, the bounded statement \begin{align*} n \in u(s) \text{ and } \forall t \leq s\, n \notin v(t) \end{align*} is true and decidable. PA proves this bounded computation, so PA proves $\theta_n$. Since $C$ extends PA, $\theta_n \in C$, and therefore $n \in S_C$. Suppose next that $n \in V$. Let $s_0$ be the first stage at which $n$ enters $V$. Since $U$ and $V$ are disjoint, $n$ does not enter $U$ at any stage. PA can prove the finite verification that there is no earlier stage witnessing entry into $U$ before $V$, and once $n$ is in $V$ at stage $s_0$, no later stage can witness "entry into $U$ before entry into $V$." Thus PA proves $\neg\theta_n$. Since $C$ is consistent, it cannot contain both $\neg\theta_n$ and $\theta_n$, so $\theta_n \notin C$. Hence $n \notin S_C$. We have proved \begin{align*} U \subseteq S_C \quad\text{and}\quad S_C \cap V = \varnothing. \end{align*} Thus a PA degree computes separators for all disjoint computably enumerable pairs.[/guided]

[step:Use separators to compute paths through infinite computable binary trees] Let $T \subseteq 2^{<\mathbb{N}}$ be an infinite computable tree. Fix a computable bijection \begin{align*} e: 2^{<\mathbb{N}} \to \mathbb{N}. \end{align*} For each $\sigma \in 2^{<\mathbb{N}}$, say that $\sigma$ is terminally bounded in $T$ if there exists $m \in \mathbb{N}$ such that no string $\tau \in T$ of length $m$ extends $\sigma$. This condition is computably enumerable because $T$ is computable and, for fixed $m$, there are only finitely many binary strings of length $m$. Define computably enumerable sets $U_T,V_T \subseteq \mathbb{N}$ as follows. Enumerate $e(\sigma)$ into $U_T$ when $\sigma^\frown 0$ is found to be terminally bounded in $T$. Enumerate $e(\sigma)$ into $V_T$ when $\sigma^\frown 1$ is found to be terminally bounded in $T$, unless $e(\sigma)$ has already been enumerated into $U_T$; if both sides are eventually found terminally bounded, enumerate only the one found first. This effective tie-breaking makes $U_T$ and $V_T$ disjoint. By the previous step, $A$ computes a separator $S_T \subseteq \mathbb{N}$ with \begin{align*} U_T \subseteq S_T \quad\text{and}\quad S_T \cap V_T = \varnothing. \end{align*} We define a sequence of finite strings $(\sigma_n)_{n \in \mathbb{N}}$ recursively. Let $\sigma_0$ be the empty string. Given $\sigma_n$, define \begin{align*} \sigma_{n+1} := \begin{cases} \sigma_n^\frown 1, & e(\sigma_n) \in S_T,\\ \sigma_n^\frown 0, & e(\sigma_n) \notin S_T. \end{cases} \end{align*} This recursion is computable from $S_T$, hence from $A$. We prove by induction on $n$ that $\sigma_n$ has arbitrarily long extensions in $T$. This is true for $\sigma_0$ because $T$ is infinite and finitely branching. Suppose $\sigma_n$ has arbitrarily long extensions in $T$. If $\sigma_n^\frown 0$ is terminally bounded, then $e(\sigma_n) \in U_T \subseteq S_T$, so the construction chooses $\sigma_n^\frown 1$. Since $\sigma_n$ has arbitrarily long extensions and the $0$-successor is terminally bounded, the $1$-successor must have arbitrarily long extensions. If $\sigma_n^\frown 1$ is terminally bounded, then $e(\sigma_n) \in V_T$, so $e(\sigma_n) \notin S_T$, and the construction chooses $\sigma_n^\frown 0$, which must have arbitrarily long extensions. If neither successor is terminally bounded, both choices have arbitrarily long extensions. Thus $\sigma_{n+1}$ has arbitrarily long extensions in $T$. Since $T$ is a tree, every string with arbitrarily long extensions in $T$ belongs to $T$. Therefore $\sigma_n \in T$ for every $n$. The unique $X \in 2^{\mathbb{N}}$ satisfying $X{\upharpoonright}n=\sigma_n$ for every $n$ is computable from $A$ and belongs to $[T]$. Hence every PA degree computes a path through every infinite computable binary tree. [/step]

[step:Show that path-computing degrees compute complete extensions of PA]Assume that $A$ computes a path through every infinite computable binary tree. Fix a computable enumeration $(\varphi_n)_{n \in \mathbb{N}}$ of all sentences in the language of PA, allowing repetitions if needed, so that every sentence occurs at least once. Also fix a computable Gödel coding of formal proofs, and let $\bot$ denote a fixed contradictory sentence, such as $0=1$. For each $\sigma \in 2^{<\mathbb{N}}$, define the finite theory \begin{align*} \Gamma_\sigma := \mathrm{PA} \cup \{\varphi_i : i < |\sigma| \text{ and } \sigma(i)=1\} \cup \{\neg\varphi_i : i < |\sigma| \text{ and } \sigma(i)=0\}. \end{align*} Define a tree $T_{\mathrm{PA}} \subseteq 2^{<\mathbb{N}}$ as follows: for $\sigma \in 2^{<\mathbb{N}}$, put $\sigma \in T_{\mathrm{PA}}$ iff for every initial segment $\tau \preceq \sigma$, there is no formal proof with Gödel code at most $|\sigma|$ of $\bot$ from $\Gamma_\tau$. This membership condition is decidable: for fixed $\sigma$, there are only finitely many initial segments $\tau \preceq \sigma$ and only finitely many proof codes at most $|\sigma|$, and checking whether a given code is a valid proof from PA together with the finite list of additional axioms in $\Gamma_\tau$ is computable. The set $T_{\mathrm{PA}}$ is a tree. If $\sigma \in T_{\mathrm{PA}}$ and $\rho \preceq \sigma$, then for every $\tau \preceq \rho$ there is no contradiction proof from $\Gamma_\tau$ with Gödel code at most $|\sigma|$. Since $|\rho| \leq |\sigma|$, there is therefore no such proof with code at most $|\rho|$, so $\rho \in T_{\mathrm{PA}}$. The tree is infinite because PA is consistent and every finite consistent extension of PA can be extended by deciding one further sentence consistently. Thus, for each $m \in \mathbb{N}$, there is a string $\sigma \in 2^{<\mathbb{N}}$ of length $m$ such that $\Gamma_\tau$ is consistent for every initial segment $\tau \preceq \sigma$. In particular, no $\Gamma_\tau$ has a contradiction proof with Gödel code at most $m=|\sigma|$, so $\sigma \in T_{\mathrm{PA}}$. By hypothesis, $A$ computes a path $Y \in [T_{\mathrm{PA}}]$. Define the theory coded by $Y$ by \begin{align*} C_Y := \mathrm{PA} \cup \{\varphi_n : Y(n)=1\} \cup \{\neg\varphi_n : Y(n)=0\}. \end{align*} Since every sentence occurs in the enumeration $(\varphi_n)_{n \in \mathbb{N}}$, for every sentence $\psi$ there is an index $n \in \mathbb{N}$ with $\varphi_n=\psi$, and the theory $C_Y$ contains either $\psi$ or $\neg\psi$. Thus $C_Y$ is complete once consistency is proved. To prove consistency, let $F \subseteq C_Y$ be a finite subset. Choose $m \in \mathbb{N}$ large enough that every non-PA sentence in $F$ is one of the decisions recorded by $Y{\upharpoonright}m$, and large enough that $m$ exceeds the Gödel code of any proposed contradiction proof from $\mathrm{PA} \cup F$. If such a proof existed, then the same proof would be a proof of $\bot$ from $\Gamma_{Y{\upharpoonright}m}$, contradicting $Y{\upharpoonright}m \in T_{\mathrm{PA}}$. Therefore every finite subset of $C_Y$ is consistent with PA, and finitary compactness for first-order proof systems gives that $C_Y$ is consistent. Also $C_Y$ extends PA by construction. Therefore $C_Y$ is a complete consistent extension of PA computable from $A$, and $a$ is a PA degree.[/step]

[guided]The delicate point is that ordinary consistency of a finite extension of PA is not decidable: absence of a proof is generally only co-computably enumerable. We avoid that problem by building a bounded-consistency tree whose definition is prefix-closed by construction. Choose the enumeration $(\varphi_n)_{n \in \mathbb{N}}$ so that every sentence of the language of PA appears at least once. For each finite binary string $\sigma \in 2^{<\mathbb{N}}$, define \begin{align*} \Gamma_\sigma := \mathrm{PA} \cup \{\varphi_i : i < |\sigma| \text{ and } \sigma(i)=1\} \cup \{\neg\varphi_i : i < |\sigma| \text{ and } \sigma(i)=0\}. \end{align*} The node $\sigma$ records decisions about the first $|\sigma|$ listed sentences, and $\Gamma_\sigma$ is the corresponding finite extension of PA. We put $\sigma$ into $T_{\mathrm{PA}}$ exactly when every initial segment $\tau \preceq \sigma$ passes the same bounded-consistency test at the longer bound $|\sigma|$: there is no proof with Gödel code at most $|\sigma|$ deriving $\bot$ from $\Gamma_\tau$. This condition is decidable. On input $\sigma$, we inspect the finitely many initial segments $\tau \preceq \sigma$ and the finitely many natural numbers $q \leq |\sigma|$, and check whether $q$ codes a valid formal proof of $\bot$ from $\Gamma_\tau$. Proof checking for a fixed formal system is computable, and each list of extra axioms in $\Gamma_\tau$ is finite and explicitly determined by $\tau$. The set $T_{\mathrm{PA}}$ is closed under initial segments. Suppose $\sigma \in T_{\mathrm{PA}}$ and $\rho \preceq \sigma$. To prove $\rho \in T_{\mathrm{PA}}$, let $\tau \preceq \rho$. Since also $\tau \preceq \sigma$, membership of $\sigma$ tells us that there is no contradiction proof from $\Gamma_\tau$ with code at most $|\sigma|$. Because $|\rho| \leq |\sigma|$, there is certainly no such proof with code at most $|\rho|$. This is precisely the membership condition for $\rho$. The tree is infinite. Since PA is consistent, any finite consistent set of added sentence-decisions can be extended by deciding one more sentence consistently: if both adding $\varphi_m$ and adding $\neg\varphi_m$ produced inconsistency, then the original finite theory would prove both $\neg\varphi_m$ and $\varphi_m$, hence would itself be inconsistent. Starting from PA and iterating this finite extension argument, for every $m \in \mathbb{N}$ there is a binary string $\sigma$ of length $m$ such that $\Gamma_\tau$ is genuinely consistent for every initial segment $\tau \preceq \sigma$. Genuine consistency implies the absence of contradiction proofs with any Gödel code, and in particular with code at most $m=|\sigma|$, so $\sigma \in T_{\mathrm{PA}}$. Now the hypothesis applies: because $T_{\mathrm{PA}}$ is an infinite computable binary tree, $A$ computes a path $Y \in [T_{\mathrm{PA}}]$. Define the theory coded by this path by \begin{align*} C_Y := \mathrm{PA} \cup \{\varphi_n : Y(n)=1\} \cup \{\neg\varphi_n : Y(n)=0\}. \end{align*} Completeness follows because every sentence $\psi$ appears as some $\varphi_n$; the path value $Y(n)$ puts either $\psi$ or $\neg\psi$ into $C_Y$. It remains to prove actual consistency, not merely bounded consistency at each finite stage. Suppose toward contradiction that some finite subset $F \subseteq C_Y$ yields a formal proof of $\bot$ from PA. Let $q \in \mathbb{N}$ be the Gödel code of that proof. Choose $m \in \mathbb{N}$ so large that every non-PA sentence in $F$ is among the decisions recorded by $Y{\upharpoonright}m$ and $m \geq q$. Then the same proof with code $q$ is a proof of $\bot$ from $\Gamma_{Y{\upharpoonright}m}$, because that finite theory contains every non-PA decision in $F$. This contradicts $Y{\upharpoonright}m \in T_{\mathrm{PA}}$, whose definition excludes all contradiction proofs from $\Gamma_{Y{\upharpoonright}m}$ with code at most $m$. Therefore every finite subset of $C_Y$ is consistent with PA, and finitary compactness for first-order proof systems gives that $C_Y$ itself is consistent. Thus $C_Y$ is a complete consistent extension of PA. Since $Y \leq_T A$ and the map $Y \mapsto C_Y$ is computable, the theory $C_Y$ is computable from $A$. Hence $a$ is a PA degree.[/guided]

[step:Identify computable trees with nonempty $\Pi^0_1$ classes] For every computable tree $T \subseteq 2^{<\mathbb{N}}$, the path set $[T]$ is a $\Pi^0_1$ class because \begin{align*} X \in [T] \iff \forall n \in \mathbb{N}\, \bigl(X{\upharpoonright}n \in T\bigr), \end{align*} and membership in $T$ is decidable. Conversely, by the definition of an [effectively closed set](/page/Effectively%20Closed%20Set) in Cantor space, every $\Pi^0_1$ class $\mathcal{P} \subseteq 2^{\mathbb{N}}$ is of the form $[T_{\mathcal{P}}]$ for some computable tree $T_{\mathcal{P}} \subseteq 2^{<\mathbb{N}}$. The class $\mathcal{P}$ is nonempty exactly when $T_{\mathcal{P}}$ is infinite. Therefore the assertion that $A$ computes a path through every infinite computable binary tree is equivalent to the assertion that $A$ computes a member of every nonempty $\Pi^0_1$ class in $2^{\mathbb{N}}$. [/step]

[step:Combine the implications] The second step and third step prove that every PA degree satisfies condition 2. The fourth step proves that condition 2 implies condition 1. The fifth step proves the equivalence of conditions 2 and 3. Hence conditions 1, 2, and 3 are equivalent. [/step]