Are there any consistency results in set theory (or in mathematics) that can be proved using nonstandard models of ZFC but not using transitive models of ZFC?
1 Answer
Yes. Harvey Friedman has identified several (natural) combinatorial statements that are equivalent to the $1$-consistency of $\mathsf{ZFC}$ or strengthenings of it via large cardinals (here, $1$-$\mathrm{Con}(T)$ is the assertion that all $\Sigma^0_1$ consequences of $T$ are true). In particular, this means that the statements in question hold in the standard model, and any model of their negation is necessarily non-standard (in fact, it is not an $\omega$-model).
See for example
Harvey M. Friedman. Finite functions and the necessary use of large cardinals, Ann. of Math. (2), 148 (3), (1998), 803–893. MR1670057 (2002b:03108).
Harvey's research has actually produced a nice variety of such statements.
If one relaxes your requirements that these be consistency results, and that any proof must necessarily involve non-standard models, a different example appears in the work of Greg Hjorth on descriptive set theory of equivalence relations, see
Greg Hjorth. Thin equivalence relations and effective decompositions, J. Symbolic Logic, 58 (4), (1993), 1153–1164. MR1253912 (95c:03119).
In his argument, Greg must analyze non-standard Ehrenfeucht-Mostowski models (coming from sharps). There is actually a different version of the argument, due to Sy Friedman and Boban Velickovic. Their argument also uses non-standard models, but their methods are different. I do not know, however, that this use is essential.