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?


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.

  • $\begingroup$ But note that all that is necessary is a single binary predicate symbol, since any first-order language can be encoded in the theory of symmetric graphs. $\endgroup$ – Rob Arthan Feb 4 '15 at 17:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.