The true but unprovable statement referred to by the theorem is often referred to as “the Gödel sentence” for the theory. It is not unique; there are infinitely many statements in the language of the theory that share the property of being true but unprovable.
So the first order axioms were invented. Godel showed that the first order axioms are not strong enough to prove all true statements about the integers. There are infinitely distinct models of the first order integers. There is only one model of the second order integers.
In the proof of the Incompleteness Theorem Godel proves a statement about an integer which is not provable in the first order system.
Humans can work in the second order system but not computers. So, from my perspective there is something different about human thought patterns. I'm not an expert and would like to know what is wrong with my reasoning.
First Theorem: "Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory."
Second Theorem: "For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent."
It wasn't that Godel proved that Peano arithmetic was incomplete that shocked mathematicians, it was that he showed that _no formal system_ could ever be complete as long as remained consistent.
Of course maybe this second order system isn't consistent, in which case there's no problem. After all, I'm fairly convinced that human reason isn't always perfectly consistent, so it makes sense that we can avoid Godel's theorems. Of course, I see no reason we couldn't make a slightly inconsistent computer either.
One can find complete axiomatic systems of the integers. It's quite easy. Just take all true statements as the axiom system. The problem is that there is no computable method for determining in such a system whether or not a given statement is an axiom.
Again, we humans can work in the second order axiom system but computers can't. So it appears there's a difference between human intelligence and computer intelligence.
Basically, what you need to prove to show that humans are intrinsically more powerful than machines is that we have the ability to generally solve noncomputable problems in a general way, ie, that we are hypercomputers.