I'm trying to describe Godel's Incompletemeness Theorem in 1 short sentence... We at the Unemployed Philosophers Guild are adding Kurt Godel to our line of illustrious finger puppets.  On the puppet tag we always have a short biography.  Below is what we have written.  Is our description of his Theorem acceptable to a mathematician/logician?
Austrian-born philosopher and logician Kurt Friedrich Gödel studied physics before publishing his famous (two) Incompleteness Theorem(s). According to Gödel, a mathematical system can’t prove or disprove every proposition within itself (it’s “incomplete”) and can’t prove itself both complete and consistent. Gödel fled Nazi Germany, renewed his friendship with fellow émigré Albert Einstein, and became a U.S. citizen. As “the most important logician since Aristotle,” Gödel influenced computer science, artificial intelligence, and philosophy of mathematics. He was devoted to operetta. 
Here is an alternate description of his work:  ...According to Gödel, if a mathematical system can prove every statement that can be constructed in the system, then there must be some contradictory statements in the system: and if there are no contradictory statements, then there are statements that cannot be proved...
Thank you!
 A: It depends on the level of precision you want to reach. 
My first remark is that "According to Gödel" feels too much like "He thought so and he said so", but maybe I'm just misunderstanding this by adding a connotation that wasn't there.
More to the point, Gödel's theorem is about formal theories that can be computed. If you want to be precise this is a detail that cannot be missed because there are many theories that are complete and prove or refute every sentence. 
A quick summary would be 

"Gödel proved that no effective [here the word "effective" allows you to vaguely state that it should be computable], expressive enough, consistent mathematical system can prove or refute every sentence: it will always be incomplete. In particular, he proved that such a system cannot prove its own consistency."

This allows you to be precise, while still being accessible (the words "effective", "expressive enough" are not detailed, so as to be understood by the non-logician), and is a good reflection of what Gödel actually did. My reformulation to "Gödel proved" (rather than "According to Gödel") is simply because I feel like this emphasizes more that this isn't just speculation or an idea he had but rather an actual theorem. 
A: The existing answers fail to capture the important criterion that the formal system in question can carry out arithmetical reasoning. If you look carefully, the most precious ingredient of all in Godel's contribution was the β-function, so I feel that it should be adequately represented.
Also, note that Godel's proof required ω-consistency, contrary to what many other suggestions are implying. However, it is hard to express that in a few words, so I would instead opt to express the weaker condition of arithmetical soundness, since that is effectively what Godel used ω-consistency for. I do not think it is fair to ascribe Rosser's strengthening of Godel's incompleteness theorems to Godel, because Godel himself did not realize it was possible even though he considered it. For both these aspects see this translation (page 17).
Also, Godel proved two incompleteness theorems.

Godel 1st: Every implementable formal system (implementable on an ideal computer) that does not prove any false arithmetical sentence (about the natural numbers) also does not prove some true arithmetical sentence.
Godel 2nd: Every implementable formal system that can perform classical arithmetical reasoning cannot prove itself consistent if it really is, but can prove this fact!

The second one can be understood to comprise external and internal forms of the incompleteness theorem. The external form asserts that if the formal system is consistent then it does not prove "⊥". The internal form asserts that the formal system S can prove "Con(S)⇒¬Prov(Con(S))" (equivalently "¬⬜⊥⇒¬⬜¬⬜⊥" in provability logic).
Note that the first theorem also applies to formal systems that cannot perform classical arithmetic (such as Presburger arithmetic), while the second theorem also applies to formal systems that are consistent but prove false arithmetical sentences (such as PA+¬Con(PA)). So if you really wish to combine them in a concise way, you will end up with a weaker theorem.

Godel 1st+2nd (short): Every useful formal system cannot prove some true arithmetical sentence, such as its own consistency.

In this short version, "useful" is supposed to encompass both implementability and arithmetical soundness and ability to perform classical arithmetic. It also omits the internal form of the 2nd completeness theorem.

For comparison, here is Rosser's strengthening of Godel's 1st incompleteness theorem.

Rosser: Every implementable formal system (implementable on an ideal computer) that can perform classical arithmetical reasoning and does not prove "$0=1$" also does not prove or disprove some arithmetical sentence (about the natural numbers).

I have purposely worded this version in a way that fits the generalization of the incompleteness theorems to all conceivable implementable formal systems that may not be classical; the only requirement is that the arithmetical fragment be classical. If you are interested, the precise details are described in this post, which also has a computability-based (but non-constructive) proof of it.
As an aside, the theory of concatenation is also essentially incomplete like PA, so incompleteness has nothing much to do with arithmetic or induction on natural numbers. This result can be generalized in the same manner:

Grzegorczyk-Zdanowski: Every implementable formal system (implementable on an ideal computer) that can perform classical reasoning about (finite) strings and does not prove a contradictory sentence about strings also does not prove or disprove some sentence about strings.


About your own attempts, the alternate is wrong because of course consistent first-order theories cannot prove "$\exists x ( x \ne x )$". The first version is ambiguous if not misleading. In history there have been mathematical systems that prove their own completeness and consistency, simply because they were inconsistent. Furthermore, there are classical theories of arithmetic that are arguably self-verifying (see this post).
A: I know there are better experts in this community, but I would propose:
"a consistent mathematical system can’t prove or disprove every mathematical proposition (it’s “incomplete”) and can’t even prove its own consistency."
The addition of 'consistent' in the beginning captures what the alternative is trying to say, and it is an important addition. The 'within itself' seems unnecessarily confusing, so I deleted that. And finally, the system not being able to prove that it is 'both consistent and complete' is not an interesting claim given that it is consistent but not not complete ... the fact that it can't prove its own consistency is the interesting claim here. 
A: This is more a very long comment rather than an answer, still I hope it could be useful.

...According to Gödel, a mathematical system can’t prove or disprove every proposition within itself (it’s “incomplete”) and can’t prove itself both complete and consistent. 

This is not correct. There are some formal systems which are consistent (i.e. they don't prove contraddictions) and are complete. 
Examples are the theories of algebrically closed fields with  fixed characteristics, the theory of real closed field, the theory of dense linearly ordered sets without maximum and minimum.
What Gödel's theorem actually states is that any formal system (i.e. first order theory) which is capable of interpreting arithmetic (which roughly means that the theory is capable of defining what is a natural number and proving the basic properties of natural numbers) and is recursively axiomatozable (that is there's an algorithm which can decide which formulas are its axioms) cannot be consistent and complete at the same time.
Gödel's theorem clearly does not apply to the above mentioned theories because they are not capable of interpret arithmetic (you can't define inside of them what a natural number is).
Also

if a mathematical system can prove every statement that can be constructed in the system, then there must be some contradictory statements in the system

This is one of the possible definition of inconsistency, it has nothing to do with Godel's theorem.
A: 
Austrian-born philosopher and logician Kurt Friedrich Gödel studied physics before publishing his famous (two) Incompleteness Theorem(s). 

Physics has nothing to do with the incompleteness theorems.  I doubt he spent as much time or effort in physics as logic, although Wikipedia suggests he did spend a lot more time on physics later in life.

According to Gödel, a mathematical system can’t prove or disprove every proposition within itself (it’s “incomplete”)

No, there are logics, even rather complex ones, that are complete and consistent.  Propositional logic and "the first-order theory of Euclidean geometry is complete and decidable" (from the link below).

and can’t prove itself both complete and consistent. 

No.  Sufficiently strong logics can not be both complete and consistent.  But any inconsistent logic can prove either of those.

Gödel fled Nazi Germany, renewed his friendship with fellow émigré Albert Einstein, and became a U.S. citizen. 

Wikipedia agrees with this.  Why don't you just say "immigrant"?

As “the most important logician since Aristotle,” 

I would say Hilbert, but some logicians would agree with you.

Gödel influenced computer science, artificial intelligence, and philosophy of mathematics. He was devoted to operetta.

CS and philosophy are a given, the other two, no idea.

Here is an alternate description of his work: ...According to Gödel, if a mathematical system can prove every statement that can be constructed in the system, then there must be some contradictory statements in the system: and if there are no contradictory statements, then there are statements that cannot be proved...

That doesn't even make sense to me.  Here is the first incompleteness theorem:
If a logic can be verified by a Turing Machine, is capable of proving all theorems of Robinson Arithmetic, and is 1-consistent; then there is a sentence $G$ such that neither $G$ is provable nor is $\lnot G$ provable in the logic.
(Small detail, but the strengthening of the statement from 1-consistent to consistent is actually due to Rosser.)
If I could say something a bit harsh, the Internet is rife with people attempting to summarize or explain Godel's Incompleteness Theorems who never bothered to really learn them.  Please don't be another.  Silence is better.  I'm not even confident about them, so I hesitated to write this.  If you wish to learn them, I find this link does a really thorough and detailed job without containing extraneous pontifications :
https://plato.stanford.edu/entries/goedel-incompleteness/

On the puppet tag we always have a short biography. 

As far as logicians with interesting lives, I find Moses Schönfinkel really compelling.  Born a poor boy in Ukraine, talented enough to eventually study even under David Hilbert, invented one of the first completely formal logics that was in some sense the grandfather of all constructive logics.  Was committed to an asylum before he was 40 and spend his later life in poverty like how he was born.  His personal papers/work were burned by his neighbors trying to stay warm because of wartime conditions.
