It is true that Godel's incompleteness theorem states that there is no complete axiomatization of arithmetic; no first order axioms can characterize the natural numbers up to isomorphism. But Godel's completeness theorem ( https://en.wikipedia.org/wiki/Gödel%27s_completeness_theorem) states that first order logic is in fact complete as a deductive system, and most automated theorem provers have the property that if a proof exists, given enough time they will eventually find it. In higher order logic the situation is reverse: the proof theory is incomplete, but you can eg characterize the natural numbers up to isomorphism. Anyway, I believe that many of your critiques apply to formal logic itself, not so much the attempts to automate formal logic.