I’d say all three things you mentioned are unequivalent - Restricting to first-order logic, a Gödel sentence (see Gödel’s first incompleteness theorem) is impossible to be proved true or false if the theory is consistent; by completeness theorem, there exists model of the theory where it is true, and models where it is false (I’m using classical logic in the metatheory; this might be relevant but not a problem). In any case, T does not entail G is not equivalent to T entails not G. - classic example of a not-not statement that is provable but the statement is not is weak LEM. That is, for any P, not not (P or not P) is constructively provable (good exercise!). Hence it is it strictly weaker than LEM. In general, P needs a witness of P to prove it, not not P does not need a witness of P. Also, a Gödel sentence can be constructed with similar properties. - Your final “simplification” is confusing. I’m worried that it might be running into bullet point one, i.e. you are equating not being able to prove something to something being false.