I Simplest independent first-order expression in PA

[ad infinitum]

What is the simplest known first-order expression known to be independent of Peano Arithmetic but decidable in ZFC for some reasonable notion of simplicity (such as number of quantifiers, nesting depth etc.); the precise definition of simplicity does not matter, I just want to see a concrete example.

 

[SSequence]

Here are few examples:
https://en.wikipedia.org/wiki/Paris–Harrington_theorem
https://en.wikipedia.org/wiki/Goodstein's_theorem

You can also search for "kirby paris hydra" or the "hydra game" and many interesting results come up. Basically it is a single player game of sorts where the player playing the game always wins "eventually". However, proving that seems to require strength beyond PA.

Based upon my limited knowledge/understanding, there is going to be a fairly large spectrum of strictly increasing (total) recursive functions whose totality will be provable in a stronger system such as ZFC but not in PA. Of course, eventually, there are going to be strictly increasing (total) recursive functions whose totality ZFC won't be able to prove either.