The self-embedding theorem of \(\text{WKL}_ 0\) and a non-standard method (Q676310)

\(\text{WKL}_0\) is a system of second-order arithmetic consisting of the axioms of discretely ordered semirings, \(\Sigma^{0}_1\) induction, \(\Delta^{0}_1\) comprehension and weak König's lemma. The paper is devoted to the proof of the following version of Friedman's embedding theorem: every countable model of \(\text{WKL}_0\) is isomorphic to a proper initial segment of itself. In particular, if \((M,X)\) is a model of \(\text{WKL}_0\) then there is a countable model \(N\) of \(I\Sigma^{0}_1\) such that \(M\) is an initial segment of \(N\) and \(X\) is the family of subsets of \(M\) coded in \(N\). The last section of the paper outlines an application of the embedding theorem to the development of the theory of continuous functions in \(\text{WKL}_0\).