Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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
add comment

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
    
"all you are asking about is whether it is possible to tell whether some string of symbols is actually a formula" Actually I asked specifically about sentences, i.e formulas where all variables are bound. After reading your answer and getting my hands on Immerman's book I start to feel confident that I was in right track. Thank you! –  rank Mar 21 '11 at 13:32
    
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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