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 well-formed formulas (wffs) in first-order logic (FOL) is decidable, because it's straightforward to translate the standard recursive syntax rules into a context free grammar, and all context free languages are decidable.

The set of sentences -- i.e. closed formulas -- of FOL is also decidable, because it's straightforward to decide whether a wff is a sentence.

But the set of sentences of FOL is not context free: if variables are encoded, say, with prme marks (so the set of variables is $x$, $x'$, $x''$, etc.), an easy application of the pumping lemma for context free languages to a sentence like $(\exists \mu)(F\mu\rightarrow F\mu)$, for a sufficiently long variable $\mu$, yields a contradiction.

So the best we can hope for, thanks to the Chomsky hierarchy, is that the set of sentences of FOL is context sensitive. Whether it is just rides on whether there is a linear bounded Turing machine that decides it.

I have two questions, then:

(1) what is the weakest Turing machine (TM) needed to decide the set of sentences of FOL? (if the answer is linear bounded, then the set of sentences of FOL is context sensitive; otherwise the best we can say is that the set of sentences of FOL is decidable)

and, more generally:

(2) is there a hierarchical structure for languages between context sensitive (type 1) and decidable? e.g., are there grammars naturally associated with polynomially bounded TM's, exponentially bounded TM's, etc.? Obviously I don't expect there to be as nice a structure here as elsewhere in the Chomsky hierarchy -- precisely because I can't seem to find a reference that talks about it. But since there is a natural ordering of Turing machines based on the amount of space they need, I'm curious about what this ordering might track on the side of grammars.

share|improve this question

2 Answers 2

up vote 1 down vote accepted

For (1): linear space is enough.

First check that the input is a well-formed formula, and build a fully parenthesized representation (which has linearly bounded size).

Then walk through the formula and each time you meet a variable search backwards in the string for a binding for that variable that is still in scope. That requires only four registers, all of logarithmic size: A pointer for walking forwards; a pointer for walking backwards, a counter for ignoring parenthesized subexpressions while walking backwards, and finally a counter for comparing the number of primes in a bound variable with the number of primes the forward pointer is looking at.

share|improve this answer

For (2): Multi-stack pushdown automata form part of the space between context-free languages and linear-bounded turing machines. They can be used to recognize finite intersections of context-free languages. There are likely other types between these automata and linear-bounded turing machines.

share|improve this answer
    
Thanks, but question (2) was about the space between linear-bounded and full-on (unconstrained) Turing machines (e.g. polynomially bounded, exponentially bounded) and their possibly associated grammars, not the space between pushdown stacks and linear-bounded. –  symplectomorphic Mar 15 '12 at 17:54
    
Oh, I'm sorry. Of course, adding a space bound like that will generate a new in-between class. They are somewhat related to the XYZ-SPACE classes in complexity, if that helps you. –  Johannes Kloos Mar 15 '12 at 17:57
    
Right, I understand the space hierarchy for TM's. I was just curious if there's any interesting way to characterize what these space classes track in terms of grammars. (Linear boundedness tracks context-sensitivity; I'm curious if there's a grammatical criterion that tracks with polynomial boundedness, etc.) –  symplectomorphic Mar 15 '12 at 18:04

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.