Major Inaccuracies in Misak's review of Journey to the Edge of Reason, a new Gödel Biography

In the Times Literary Supplement there is a review of a new biography of Gödel by philosopher Cheryl Misak. The review is called 'What are the limits of logic? How a groundbreaking logician lost control'. This paragraph contains two major inaccuracies:

Gödel proved that if a statement in first-order logic is well formed (that is to say, it follows the syntactic rules for the formal language correctly), then there is a formal proof of it. But his second doctorate, or Habilitation, published in 1931, showed that in any formal system that includes arithmetic, there will always be statements that are both true and unprovable. The answer to the Entscheidungsproblem was, therefore, negative.

The first one is that being well formed is like being grammatically correct - among the well formed formulas of first-order logic, there are formulas that are false no matter what (false on all models or interpretations), formulas that can go either way, and formulas that are true no matter what (these ones are often called logical truths, or logically valid formulas). What Gödel showed is that for every logical truth, there is a proof that it's a logical truth. 

The second major inaccuracy is that the answer to the decision problem (Entscheidungsproblem) is not shown to be negative by the incompleteness theorem that Misak alludes to. The negative answer became known only in 1936, when Alonzo Church and Alan Turing independently showed it.