True and unprovable vs. unprovable and unrefutable

Question

I have seen two versions of incompleteness that follow from the correctness of a system and its power (i.e. of a system that satisfies the assumptions of Gödel's first incompleteness theorem).

1. There is a sentence which is true but unprovable.
2. There is a sentence which is unprovable and unrefutable.

Does one of these statements follow from the other? The first one does not need a definition of unrefutable, so it seems no. But then, why are not both statements referenced equally often in literature? They seem to be equally interesting?

Here, the system can be any general system, not necessarily talking about natural numbers and not necessarily having operators like "not". We define sets of sentences, true sentences, provable sentences (if the system is correct, this will be a subset of true sentences), refutable sentences (if correct, then these are not true), predicates and an encoding function (which sends a predicate and a natural number to a sentence and can be used to express sets of natural numbers).

Answer 1

When saying "true" we mean "true in a certain model". In the context of arithmetic, "true" means in $\Bbb N$.

If there is a sentence which is true but not provable, then it means it is neither provable nor refutable. On the other hands, if $\varphi$ is neither provable nor refutable, either $\varphi$ or $\lnot\varphi$ is a sentence true in $\Bbb N$, and therefore exactly one of $\varphi,\lnot\varphi$ is true; but neither is provable.

Answer 2

See this post for a precise generalization of the incompleteness theorems. $ \def\nn{\mathbb{N}} $ There I have defined an arithmetical sentence over a formal system $S$ that interprets arithmetic to be of the form $ι(φ)$ for some sentence $φ$ over PA, where $ι$ is the translation that witnesses that $S$ interprets arithmetic. Similarly we say that an arithmetical sentence $ι(φ)$ over $S$ is true iff $\nn \vDash φ$. For an interesting situation we also define that $S$ refutes an arithmetical sentence $ι(φ)$ iff $S$ proves $ι(\neg φ)$.

Then indeed if $S$ also has decidable proof validity then it satisfies both properties you mentioned, and moreover it is trivial that (2) implies (1) even if $S$ does not have decidable proof validity. But the reverse implication may not hold. For example, let $N'$ be any non-standard model of PA, and $T$ be the complete theory of $N'$, then there is some sentence $φ$ over PA that is true in $\nn$ but false in $N'$, and hence $ι(φ)$ is true but unprovable in $T$, where $ι$ here is of course the identity translation.