Godel’s Incompleteness Theorem states that any omega-consistent recursive theory in the language of first-order arithmetic is incomplete. But there is a weaker version of Godel’s Theorem that is often proved first in logic books because it’s easier to prove: any recursive theory in the language of arithmetic which is sound is incomplete.
My question is, what subsystem of second-order arithmetic suffices to prove this weak Godel’s Theorem? Certainly some amount of second-order arithmetic is required, given that we need to be able to talk about the truth predicate of first-order arithmetic.