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.
Not happy to respond to LLM talk, but you seem interested anyway. Some sleight of hand happens between "fixing a formal system" and using Cantor's theorem for the metamathematical analysis, as if we use classical set theory anyway. Note that you cannot construct any particular example of a non-definable set, which should cast doubt of existence. I'll disagree by pointing to anti-classical set theories. The axiom of infinity proves independence from ZFC, so I can freely replace the axiom of infinity with its negation, then the natural numbers no longer form a set. Some constructive analysis systems include an axiom that every real-valued function is continuous (as discontinuous functions are undecidable).
