Take the 2-minute tour ×

The set of wffs of first-order logic is recursive. Taking that checking if a wff is a sentence is straightforward I take that the set of sentences of FO is also recursive.

If we add FO the least fixed point operator, does the set of sentences stay recursive? I guess yes, but I haven't seen this proved anywhere. Where can I find a (rigorous) proof?

What about other logics, say MSO?

share|improve this question

1 Answer 1

up vote 4 down vote accepted

As long as the set of sentences is given by any "reasonable" grammar, it will be decidable. The same proof as usual can be modified: you just provide a parsing algorithm for the language. It's sufficient to show that the language has a context-free grammar, which it will even if you add more function symbols. It doesn't matter what the symbols mean; all you are asking about is whether it is possible to tell whether some string of symbols is actually a formula.

The set of logically valid formulas for first-order logic is not decidable, however. It is only computably enumerable, and that follows from the completeness theorem for first-order logic. So if you added new symbols with different semantics, in a way that made the completeness theorem fail, then the set of logically valid formulas in your new language might not be computably enumerable. This is the case for second order logic, where the set of logically valid formulas (in full second-order semantics) is very far from being computably enumerable.

share|improve this answer
Once you can tell whether something is a formula, it's a very small step to check whether the variables are all bound; you just make a parse tree and walk up it from the leaves to the root. –  Carl Mummert Mar 21 '11 at 13:49

Your Answer

