Theorem 2.2.25 (Tennenbaum). Assuming that:

  • M=(M,⊕,⊗,≼,n0,n1) a countable non-standard model of PA⁡

Then ⊕ is not recursive.