On Decidability of first order logic

Question

why we need the beta-function to show that arithmetic (the theory of the standard model) is undecidable, but that no beta-function is needed for shown that universal validity in first-order logic is undecidable?

Answer 1

The $\beta$ function is used to express finite sequences in the language of arithmetic, showing that wffs in this language can (effectively) quantify over such sequences. This is then used to construct a family of sentences whose truth values are hard to decide.

However, when we're showing that first-order logic in general is undecidable, we don't need to stick to the language of arithmetic -- we can use as many function and predicate letters as we want to, and supply our own (finite) axiomatization of how we want them to behave. This gives us plenty of opportunity to write wffs that speak about finite sequences other than by the $\beta$ function, many of which are more intuitive than the $\beta$ trick too.

All of the ways to prove undecidability of first-order logic I can think of on short notice do depend on some way to formalize finite sequences. It's just that the $\beta$ trick isn't needed for doing so in the rich language of FOL.