The division you see has to do with the level of conservativity of the theories in question. On the one hand, the theory ZFC + Con(ZFC) is not $\Pi^0_1$-conservative over ZFC since Con(ZFC) is a $\Pi^0_1$ sentence which is not provable from ZFC. On the other hand, CH is $\Pi^0_1$-conservative over ZFC since ZFC + CH and ZFC prove exactly the same arithmetical facts. Indeed, by the Shoenfield Absoluteness Theorem, ZFC and ZFC + CH prove exactly the same $\Sigma^1_2$ facts. In general, forcing arguments will not affect $\Sigma^1_2$ facts and so any statement whose independence is proved by means of forcing will be $\Sigma^1_2$-conservative over ZFC. By contrast, large cardinal hypotheses are not $\Pi^0_1$-conservative over ZFC.
An example of a natural statement that is independent of PA but nevertheless true is the Paris–Harrington Theorem, which is equivalent to the 1-consistency of PA. In other words, the statement is equivalent to the statement that every PA-provable $\Sigma^0_1$ sentence is true.
Here is a result along the lines you are requesting, which
I find beautifully paradoxical.
Theorem. Every model of ZFC has an element that is a
model of ZFC. That is, every $M\models ZFC$ has an element
$m$, which $M$ thinks is a structure in the language of set
theory, a set $m$ and a binary relation $e$ on $m$, such
that if we consider externally the set of objects $\bar
m=\{\ a\ |\ M\models a\in m\ \}$ with the relation $a\mathrel{\bar e}
b\leftrightarrow M\models a\mathrel{e} b$, then $\langle
\bar m,\bar e\rangle\models ZFC$.
Many logicians instinctively object to the theorem, on the
grounds of the Incompleteness theorem, since we know that
$M$ might model $ZFC+\neg\text{Con}(ZFC)$. And it is true
that this kind of $M$ can have no model that $M$ thinks is
a ZFC model. The paradox is resolved, however, by the kind
of issues mentioned in your question and the other answers,
that the theorem does not claim that $M$ agrees that $m$ is
a model of the ZFC of $M$, but only that it externally is a
model of the (actual) ZFC. After all, when $M$ is
nonstandard, it may be that $M$ does not agree that $m$
satisfies ZFC, even though $m$ actually is a model of ZFC,
since $M$ may have many non-standard axioms that it insists
upon.
Proof of theorem. Suppose that $M$ is a model of ZFC. Thus,
in particular, ZFC is consistent. If it happens that $M$ is
$\omega$-standard, meaning that it has only the standard
natural numbers, then $M$ has all the same proofs and
axioms in ZFC that we do in the meta-theory, and so $M$
agrees that ZFC is consistent. In this case, by the
Completeness theorem applied in $M$, it follows that there
is a model $m$ which $M$ thinks satisfies ZFC, and so it
really does.
The remaining case occurs when $M$ is not
$\omega$-standard. In this case, let $M$ enumerate the
axioms of what it thinks of as ZFC in the order of their Goedel numbers. An initial segment of
this ordering consists of the standard axioms of ZFC. Every
finite collection of those axioms is true in some
$(V_\alpha)^M$ by an instance of the Reflection theorem.
Thus, since $M$ cannot identify the standard cut of its
natural numbers, it follows (by overspill) that there is
some nonstandard initial segment of this enumeration that
$M$ thinks is true in some $m=(V_\alpha)^M$. Since this
initial segment includes all actual instances of the ZFC
axioms, it follows that $m$ really is a model of ZFC, even
if $M$ does not agree, since it may think that some
nonstandard axioms might fail in $M$. $\Box$
I first learned of this theorem from Brice Halimi, who was visiting in New York in 2011, and who subsequently published his argument in:
Halimi, Brice, Models as universes, Notre Dame J. Formal Logic 58, No. 1, 47-78 (2017). ZBL06686417.
Note that in the case that $M$ is $\omega$-nonstandard, then we actually get that a rank initial segment $(V_\alpha)^M$ is a model of ZFC. This is a very nice transitive set from $M$'s perspective.
There are other paradoxical situations that occur with countable computably saturated models of ZFC. First, every such M contains rank initial segment $(V_\alpha)^M$, such that externally, $M$ is isomorphic to $(V_\alpha)^M$. Second, every such $M$ contains an element $m$ which $M$ thinks is an $\omega$-nonstandard model of a fragment of set theory, but externally, we can see that $M\cong m$. Switching perspectives, every such $M$ can be placed into another model $N$, to which it is isomorphic, but which thinks $M$ is nonstandard.
Best Answer
Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.
Note: The following is explained in Mike O'Connor's article, but I think I need to clarify why ZFC is not the ideal base theory to do this and why PA is a better candidate.
The idea is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) This is why PA, or more generally any recursively axiomatizable extension of PA, provides a more natural environment for the analysis of such statements. For example, instead of ZFC, you may as well use the purely arithmetical part of ZFC.
There is also an even more fundamental problem with transfinite iterates. Given a recursive presentation of a theory T, the iterates T0 = T, T1 = T0 + Con(T0), T2 = T1 + Con(T1), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of Tω or Tω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.
These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend these to subsystems of second-order arithmetic, but there and in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations and take advantage of their richer surroundings.