Hindman's theorem and idempotent types

Uri Andrews, Isaac Goldbring

Motivated by a question of Di Nasso, we prove that Hindman's theorem is equivalent to the existence of idempotent types in countable complete extensions of Peano Arithmetic.