[proofplan] We build a countable Turing ideal $\mathcal S$ beginning with the computable sets and repeatedly close under weak König witnesses: whenever an infinite binary tree is computable from a set already in the ideal, we add an infinite path through it. The relativised [Low Basis Theorem](/theorems/5436) lets us choose these paths so that every finite join appearing in the construction remains low. Hence the final ideal satisfies $\mathsf{WKL}_0$, but it omits [the halting problem](/theorems/1823) $\varnothing'$, so it cannot satisfy $\mathsf{ACA}_0$, whose $\omega$-models are exactly the Turing ideals closed under Turing jump. [/proofplan] [step:Recall the model-theoretic characterisations to be used] A set $\mathcal S \subseteq 2^{\mathbb N}$ is a Turing ideal if it satisfies the following two closure properties: \begin{align*} X \in \mathcal S \text{ and } Y \leq_T X &\implies Y \in \mathcal S,\\ X,Y \in \mathcal S &\implies X \oplus Y \in \mathcal S. \end{align*} Here $X \oplus Y \subseteq \mathbb N$ denotes the Turing join of $X$ and $Y$. The associated second-order structure $(\mathbb N,\mathcal S)$ is an $\omega$-model because its first-order part is the standard natural numbers and its second-order part is $\mathcal S$. We shall use the following standard reverse-mathematical facts. First, by the omega-model characterisation of [Weak Konig's Lemma](/page/Weak%20Konig%20Lemma), an $\omega$-model $(\mathbb N,\mathcal S)$ satisfies $\mathsf{WKL}_0$ exactly when $\mathcal S$ is a Turing ideal with the path property: for every $A \in \mathcal S$ and every infinite binary tree $T \subseteq 2^{<\mathbb N}$ with $T \leq_T A$, there is an infinite path $P \in \mathcal S$ through $T$. Second, by the omega-model characterisation of [arithmetical comprehension](/page/Arithmetical%20Comprehension), an $\omega$-model $(\mathbb N,\mathcal S)$ satisfies $\mathsf{ACA}_0$ exactly when $\mathcal S$ is closed under Turing jump: for every $A \in \mathcal S$, the jump $A'$ belongs to $\mathcal S$. Third, we use the [relativised Low Basis Theorem](/page/Low%20Basis%20Theorem): if $A \subseteq \mathbb N$ and $T \subseteq 2^{<\mathbb N}$ is an infinite binary tree computable from $A$, then $T$ has an infinite path $P \in 2^{\mathbb N}$ such that $A \oplus P$ is low relative to $A$, meaning \begin{align*} (A \oplus P)' \equiv_T A'. \end{align*} In particular, if $A$ is low, then \begin{align*} (A \oplus P)' \equiv_T A' \equiv_T \varnothing', \end{align*} so $A \oplus P$ is low. Fourth, we use the countable low Scott-set [extension theorem](/theorems/59), which is the uniform countable form of the relativised Low Basis Theorem: if $\mathcal I \subseteq 2^{\mathbb N}$ is a countable Turing ideal and every member of $\mathcal I$ is low, then there is a countable Turing ideal $\mathcal J \subseteq 2^{\mathbb N}$ such that $\mathcal I \subseteq \mathcal J$, every member of $\mathcal J$ is low, and for every $A \in \mathcal I$ and every infinite binary tree $T \subseteq 2^{<\mathbb N}$ with $T \leq_T A$, the ideal $\mathcal J$ contains an infinite path through $T$. This theorem packages the standard countable construction of a low Scott set extending a given countable low ideal. [guided] The construction is phrased in terms of Turing ideals because $\omega$-models of subsystems of second-order arithmetic are controlled by their second-order parts. A Turing ideal is exactly the closure condition needed for recursive comprehension and finite joins inside the model: if a set is available, then every set computable from it is available, and if two sets are available, their join is available. The $\mathsf{WKL}_0$ requirement has a concrete form in an $\omega$-model. A binary tree $T \subseteq 2^{<\mathbb N}$ is represented by a set of finite binary strings. If $T$ is infinite and computable from some oracle $A \in \mathcal S$, then weak König's lemma asks for an infinite path $P \in 2^{\mathbb N}$ through $T$ that is also in $\mathcal S$. Thus, to make an $\omega$-model of $\mathsf{WKL}_0$, it is enough to make sure the ideal contains paths through all infinite binary trees computable from its members. The obstruction to $\mathsf{ACA}_0$ is also concrete. Arithmetical comprehension over an $\omega$-model is equivalent to closure under Turing jump. In particular, since the computable set $\varnothing$ will belong to our ideal, any $\omega$-model of $\mathsf{ACA}_0$ with this same first-order part would have to contain $\varnothing'$. Therefore the construction will deliberately satisfy all weak König requirements while keeping $\varnothing'$ out. The key tool is the relativised Low Basis Theorem. It says that if an infinite binary tree is computable from an oracle $A$, then there is a path $P$ through the tree such that $A \oplus P$ is low relative to $A$, i.e. \begin{align*} (A \oplus P)' \equiv_T A'. \end{align*} When $A$ is already low, this gives \begin{align*} (A \oplus P)' \equiv_T A' \equiv_T \varnothing', \end{align*} so the enlarged oracle $A \oplus P$ is still low. This matters because a low set cannot compute $\varnothing'$. Indeed, if $B$ is low and $\varnothing' \leq_T B$, then monotonicity of the jump gives \begin{align*} \varnothing'' \leq_T B', \end{align*} while lowness gives $B' \equiv_T \varnothing'$, contradicting the [strictness of the Turing jump](/theorems/5417) hierarchy. Thus low-basis choices give paths without accidentally adding the halting problem. [/guided] [/step] [step:Construct an increasing sequence of countable low Turing ideals] Let $\mathcal S_0$ be the collection of computable subsets of $\mathbb N$. Then $\mathcal S_0$ is a countable Turing ideal, and every member of $\mathcal S_0$ is low. Assume $\mathcal S_n$ has been constructed as a countable Turing ideal whose members are all low. Apply the countable low Scott-set extension theorem to the countable low ideal $\mathcal S_n$. Its hypotheses are satisfied because $\mathcal S_n$ is countable, is a Turing ideal, and consists only of low sets. We obtain a countable Turing ideal $\mathcal S_{n+1}$ such that \begin{align*} \mathcal S_n \subseteq \mathcal S_{n+1}, \end{align*} such that every member of $\mathcal S_{n+1}$ is low, and such that for every $A \in \mathcal S_n$ and every infinite binary tree $T \subseteq 2^{<\mathbb N}$ with $T \leq_T A$, there is an infinite path $P \in \mathcal S_{n+1}$ through $T$. For concreteness, the tree requirements covered at this stage may be indexed as follows. Since $\mathcal S_n$ is countable, the set of pairs $(A,e)$ with $A \in \mathcal S_n$ and $e \in \mathbb N$ is countable, where $e$ ranges over Turing functionals $\Phi_e$ and $\Phi_e^A$ is read as a putative characteristic function for an $A$-computable binary tree. The extension theorem branches according to the true infinitude status of the tree defined by $\Phi_e^A$; no decidable test for infinitude is being asserted. [guided] We start with the computable sets because they form the smallest second-order part available in any $\omega$-model with the standard natural numbers. Define $\mathcal S_0$ to be the collection of computable subsets of $\mathbb N$. This is countable, is downward closed under Turing reducibility, and is closed under Turing join, so it is a Turing ideal. Every computable set $X$ is low because $X \equiv_T \varnothing$ implies \begin{align*} X' \equiv_T \varnothing'. \end{align*} Now suppose $\mathcal S_n$ is already a countable Turing ideal and every set in $\mathcal S_n$ is low. The next layer must add paths for all weak Konig requirements generated by the current ideal, but it must not add a set that computes the halting problem. This is exactly the role of the countable low Scott-set extension theorem. We verify its hypotheses: $\mathcal S_n$ is countable by the inductive construction, it is a Turing ideal by the inductive construction, and every member of it is low by the inductive construction. Therefore the theorem gives a countable Turing ideal $\mathcal S_{n+1}$ with \begin{align*} \mathcal S_n \subseteq \mathcal S_{n+1}, \end{align*} with every member of $\mathcal S_{n+1}$ low, and with the following path property relative to the previous layer: whenever $A \in \mathcal S_n$ and $T \subseteq 2^{<\mathbb N}$ is an infinite binary tree satisfying $T \leq_T A$, there is an infinite path $P \in \mathcal S_{n+1}$ through $T$. The indexing convention behind this statement is standard but worth making explicit. A natural number $e \in \mathbb N$ indexes a Turing functional $\Phi_e$. For an oracle $A \subseteq \mathbb N$, the computation $\Phi_e^A$ may define the characteristic function of a set of finite binary strings, and when that set is closed under initial segments we regard it as an $A$-computable binary tree. The construction is not claiming that infinitude of such a tree is decidable; it branches according to the actual mathematical truth of whether the tree is infinite. This is an existence construction of ideals, not a computable procedure for recognising infinite trees. [/guided] [/step] [step:Take the union and verify it is a countable Turing ideal] Define \begin{align*} \mathcal S := \bigcup_{n=0}^{\infty} \mathcal S_n. \end{align*} Since each $\mathcal S_n$ is countable, the set $\mathcal S$ is countable. We verify that $\mathcal S$ is a Turing ideal. Let $X \in \mathcal S$ and $Y \leq_T X$. Choose $n \in \mathbb N$ such that $X \in \mathcal S_n$. Since $\mathcal S_n$ is a Turing ideal, $Y \in \mathcal S_n \subseteq \mathcal S$. Let $X,Y \in \mathcal S$. Choose $m,n \in \mathbb N$ such that $X \in \mathcal S_m$ and $Y \in \mathcal S_n$. Put $r := \max\{m,n\}$. Since the sequence $(\mathcal S_n)_{n \in \mathbb N}$ is increasing, both $X$ and $Y$ belong to the Turing ideal $\mathcal S_r$. Hence $X \oplus Y \in \mathcal S_r \subseteq \mathcal S$. Therefore $\mathcal S$ is a Turing ideal. [guided] The union is countable because it is a [countable union of countable sets](/theorems/755): \begin{align*} \mathcal S = \bigcup_{n=0}^{\infty} \mathcal S_n. \end{align*} We next check the two defining closure properties of a Turing ideal. For downward closure, take $X \in \mathcal S$ and $Y \leq_T X$. By definition of the union, there is $n \in \mathbb N$ with $X \in \mathcal S_n$. Since $\mathcal S_n$ is itself a Turing ideal, it is downward closed under Turing reducibility, so $Y \in \mathcal S_n$. Because $\mathcal S_n \subseteq \mathcal S$, this gives $Y \in \mathcal S$. For closure under joins, take $X,Y \in \mathcal S$. Choose $m,n \in \mathbb N$ such that $X \in \mathcal S_m$ and $Y \in \mathcal S_n$, and define \begin{align*} r := \max\{m,n\}. \end{align*} The ideals are increasing, so $\mathcal S_m \subseteq \mathcal S_r$ and $\mathcal S_n \subseteq \mathcal S_r$. Hence both $X$ and $Y$ are members of $\mathcal S_r$. Since $\mathcal S_r$ is a Turing ideal, it contains their Turing join $X \oplus Y$. Thus $X \oplus Y \in \mathcal S_r \subseteq \mathcal S$. These two closure checks prove that $\mathcal S$ is a Turing ideal. [/guided] [/step] [step:Verify the path property for every tree computable from the final ideal] Let $A \in \mathcal S$, and let $T \subseteq 2^{<\mathbb N}$ be an infinite binary tree such that $T \leq_T A$. Choose $n \in \mathbb N$ with $A \in \mathcal S_n$. By the defining property of the extension from $\mathcal S_n$ to $\mathcal S_{n+1}$, applied to this oracle $A$ and this infinite $A$-computable tree $T$, there is an infinite path $P \in \mathcal S_{n+1}$ through $T$. Since $\mathcal S_{n+1} \subseteq \mathcal S$, this path satisfies $P \in \mathcal S$. Thus every infinite binary tree computable from a member of $\mathcal S$ has a path in $\mathcal S$. By the omega-model characterisation of $\mathsf{WKL}_0$, the structure $(\mathbb N,\mathcal S)$ satisfies $\mathsf{WKL}_0$. [guided] To verify weak Konig's lemma inside the final $\omega$-model, fix an arbitrary oracle $A \in \mathcal S$ and an arbitrary infinite binary tree $T \subseteq 2^{<\mathbb N}$ such that $T \leq_T A$. Because $A$ lies in the union defining $\mathcal S$, there is some $n \in \mathbb N$ with $A \in \mathcal S_n$. The construction of $\mathcal S_{n+1}$ was designed precisely to handle all tree requirements whose oracle lies in $\mathcal S_n$. The extension theorem gives the following conclusion for this particular $A$ and $T$: since $A \in \mathcal S_n$ and $T$ is an infinite binary tree computable from $A$, there exists an infinite path $P \in \mathcal S_{n+1}$ through $T$. Since the sequence of ideals is increasing and $\mathcal S_{n+1} \subseteq \mathcal S$, we get \begin{align*} P \in \mathcal S. \end{align*} This proves the path property for every infinite binary tree computable from a member of $\mathcal S$. The omega-model characterisation of $\mathsf{WKL}_0$ applies because we have already proved that $\mathcal S$ is a Turing ideal. Therefore $(\mathbb N,\mathcal S)$ satisfies $\mathsf{WKL}_0$. [/guided] [/step] [step:Keep the halting problem out of the final ideal] Every member of every $\mathcal S_n$ is low by the inductive construction. Hence every $X \in \mathcal S$ is low: \begin{align*} X' \equiv_T \varnothing'. \end{align*} We claim that $\varnothing' \notin \mathcal S$. Suppose, toward a contradiction, that $\varnothing' \in \mathcal S$. Since every member of $\mathcal S$ is low, this would imply \begin{align*} (\varnothing')' \equiv_T \varnothing'. \end{align*} But $(\varnothing')' = \varnothing''$, and the strictness of the Turing jump hierarchy gives \begin{align*} \varnothing' <_T \varnothing''. \end{align*} This contradiction proves $\varnothing' \notin \mathcal S$. [guided] The construction preserves lowness at every layer: $\mathcal S_0$ consists of computable sets, hence low sets, and the countable low Scott-set extension theorem ensures that if every member of $\mathcal S_n$ is low, then every member of $\mathcal S_{n+1}$ is low. Therefore every set in the union $\mathcal S$ is low. In symbols, for each $X \in \mathcal S$, \begin{align*} X' \equiv_T \varnothing'. \end{align*} Now suppose for contradiction that the halting problem $\varnothing'$ belonged to $\mathcal S$. Since every member of $\mathcal S$ is low, applying lowness to the particular member $X = \varnothing'$ would give \begin{align*} (\varnothing')' \equiv_T \varnothing'. \end{align*} The left-hand side is $\varnothing''$. Thus the supposition would imply \begin{align*} \varnothing'' \equiv_T \varnothing'. \end{align*} This contradicts the strictness of the Turing jump hierarchy, which states \begin{align*} \varnothing' <_T \varnothing''. \end{align*} Therefore $\varnothing' \notin \mathcal S$. [/guided] [/step] [step:Conclude that the model satisfies $\mathsf{WKL}_0$ but not $\mathsf{ACA}_0$] The preceding steps show that $\mathcal S$ is a countable Turing ideal with the path property for all infinite binary trees computable from its members. Therefore $(\mathbb N,\mathcal S)$ is an $\omega$-model of $\mathsf{WKL}_0$. Since $\varnothing$ is computable, $\varnothing \in \mathcal S_0 \subseteq \mathcal S$. If $(\mathbb N,\mathcal S)$ were an $\omega$-model of $\mathsf{ACA}_0$, then the jump-closure characterisation of $\mathsf{ACA}_0$ for $\omega$-models would imply \begin{align*} \varnothing' \in \mathcal S. \end{align*} This contradicts the previous step. Hence $(\mathbb N,\mathcal S)$ is not an $\omega$-model of $\mathsf{ACA}_0$. This proves that there is an $\omega$-model of $\mathsf{WKL}_0$ that is not a model of $\mathsf{ACA}_0$. [guided] We now assemble the two model-theoretic conclusions. First, $\mathcal S$ is a Turing ideal, and for every $A \in \mathcal S$ every infinite binary tree computable from $A$ has a path in $\mathcal S$. These are exactly the hypotheses in the omega-model characterisation of $\mathsf{WKL}_0$. Therefore the second-order structure $(\mathbb N,\mathcal S)$ satisfies $\mathsf{WKL}_0$. Second, $\varnothing$ is computable, so $\varnothing \in \mathcal S_0 \subseteq \mathcal S$. If $(\mathbb N,\mathcal S)$ satisfied $\mathsf{ACA}_0$, then the omega-model characterisation of $\mathsf{ACA}_0$ would force $\mathcal S$ to be closed under Turing jump. Applying that closure to $\varnothing \in \mathcal S$ would give \begin{align*} \varnothing' \in \mathcal S. \end{align*} But the preceding step proved $\varnothing' \notin \mathcal S$. This contradiction shows that $(\mathbb N,\mathcal S)$ is not a model of $\mathsf{ACA}_0$. Thus there exists an $\omega$-model of $\mathsf{WKL}_0$ that is not a model of $\mathsf{ACA}_0$. [/guided] [/step]