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.
