What is a model of $RCA_0$ plus the negation of the weak Konig's lemma?
This came up in conversation with someone and I couldn't find anything with a cursory search.
What is a model of $RCA_0$ plus the negation of the weak Konig's lemma?
This came up in conversation with someone and I couldn't find anything with a cursory search.
Elaborating on Carl Mummert's comment, the standard example is REC - this is the $\omega$-model (= standard first-order part) with just the recursive (or computable) sets. It is the smallest $\omega$-model of RCA$_0$.
To see that REC doesn't satisfy Weak Konig's Lemma, it's enough to show that there is a computable tree $T\subseteq 2^{<\omega}$ with no computable path. There are many well-known examples of such trees, the most natural in my opinion being the DNR$_2$ tree: a finite binary sequence $\sigma$ is on the DNR$_2$ tree iff for each $i<\vert\sigma\vert$ we have $$\neg(\Phi_i(i)[\vert\sigma\vert]\downarrow=\sigma(i))$$ where $(\Phi_i)_{i\in\omega}$ is some reasonable enumeration of the partial recursive binary functions. Since the defining property only refers to bounded-length computations, this tree is indeed computable. That is, the DNR$_2$ tree is in REC.
So why does REC think it has no paths? Well, the DNR$_2$ tree is trying to "diagonalize" against all the computable functions (and indeed "DNR" stands for "Diagonally Non-Recursive" - the "$2$" is because we're looking at binary functions): if $f$ is a path through the DNR$_2$ tree, we know that $f$ can't be computed by $\Phi_e$ because the $e$th bit of $f$ is different from the $e$th bit of the real computed by $\Phi_e$ (if the latter even exists!). Such functions obviously exist, but just as obviously aren't computable, so the DNR$_2$ tree is infinite but has no computable path.
Incidentally, the DNR$_2$ tree is "universal" in a precise sense: if $T$ is an infinite computable binary tree, then any path through the DNR$_2$ tree computes a path through $T$, and this is uniform in an index for $T$. This is a good exercise. HINT: for a computable tree $S$ we can find an $e_S$ such that $\Phi_{e_S}(e_S)\downarrow=1$ iff the "left half" of $S$ dies before the "right half" of $S$ ...