There exist subsets of the natural numbers which are infinite, but which are not finitely definable in first-order arithmetic.
1. Fix a formal system S. In the LLM example, it uses first-order arithmetic, but I don't see why we wouldn't be able to use ZFC.
2. Let D be the set of subsets of the natural numbers N which are definable by a finite formula in S.
3. There are countably many finite formulas, so |D| <= |N|.
4. Cantor's theorem says that the size of the power set of N is greater than |N|.
5. Therefore there must be subsets of N which are not definable by a finite formula in S.
If you disagree with this, I would be interested to know.https://en.wikipedia.org/wiki/Axiom_of_infinity#Independence
https://en.wikipedia.org/wiki/Constructive_analysis#Anti-cla...