- #1

- 17

- 1

## Main Question or Discussion Point

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.