The self-embedding theorem of WKL0 and a non-standard method Original Research Article

We prove that every countable non-standard model of WKL0 has a proper initial part isomorphic to itself. This theorem enables us to carry out non-standard arguments over WKL0.