I have 3 examples but each of them has its own flaws. They are consistency of Peano arithmetics, Goodstein's Theroem and *-Ramsey's Theorem. I would love something what can be explained together with its proof in set theory in, say, 20 minutes to a person interested math but not knowing the mathematical logics or set theory -- something what would elegantly demonstrate the power the infinity.
What I dislike on mentioned examples:
- Consistency of Peano arithmetics: I think that this one is the worst one because it is pretty difficult to even state. And the proof by construction of a model feels a bit like a cheat.
- Goodstein's Theorem: If we state it by cutting hydra, it can be easily confused with something provable in PA but the base-$n$ definition is nice. A bigger problem is that the proof requires ordinal numbers. They are quite difficult to explain and if I introduced them really briefly, the listener wouldn't feel very convinced.
- Paris–Harrington theorem: I really like the proof of infinite Ramsey theorem. If it ended there, I would be satisfied. Unfortunately then the technical compactness principle is required. And those things which are trivial but technical are the most difficult to explain.
So, I am interested whether the property "Being provable in ZFC but not in PA" can be distilled (perhaps from 2. and 3.) to something with a proof simple enough.