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).
- There is a sentence which is true but unprovable.
- 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).