Isn't this broader than the limitations of first order logic? After Turing we know that no matter what formal system of axioms and rules of inference one choses(as long as these can be mechanically done) then there will be some true statements the system wont be able to see. (does the nth turing machine stop?, does a particular diophantine eqn have integer solutions?)